diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 5983dcec61..953247847b 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -138,14 +138,17 @@ theorem symm {A : (Type U)} {a b : A} (H : a = b) : b = a
 theorem trans {A : (Type U)} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
 := subst H1 H2
 
-theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a
-:= substp (fun h : A → B, f a = h a) (refl (f a)) H
+theorem hcongr1 {A : (Type U)} {B : A → (Type U)} {f g : ∀ x, B x} (H : f = g) (a : A) : f a = g a
+:= substp (fun h, f a = h a) (refl (f a)) H
+
+theorem congr1 {A B : (Type U)} {f g : A → B} (H : f = g) (a : A) : f a = g a
+:= hcongr1 H a
 
 theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b
 := substp (fun x : A, f a = f x) (refl (f a)) H
 
 theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
-:= subst (congr2 f H2) (congr1 b H1)
+:= subst (congr2 f H2) (congr1 H1 b)
 
 theorem true_ne_false : ¬ true = false
 := assume H : true = false,
@@ -621,7 +624,7 @@ theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
 theorem not_implies (a b : Bool) : ¬ (a → b) ↔ a ∧ ¬ b
 := calc (¬ (a → b)) = ¬ (¬ a ∨ b)  : { imp_or a b }
                  ... = ¬ ¬ a ∧ ¬ b  : not_or (¬ a) b
-                 ... = a ∧ ¬ b      : by simp
+                 ... = a ∧ ¬ b      : congr2 (λ x, x ∧ ¬ b) (not_not_eq a)
 
 theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
 := (not_implies a b) ◂ H
diff --git a/src/builtin/num.lean b/src/builtin/num.lean
index 8b73e7ce2d..79e6d4216f 100644
--- a/src/builtin/num.lean
+++ b/src/builtin/num.lean
@@ -446,7 +446,7 @@ theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A)
           calc prim_rec x f zero = prim_rec_fun x f zero (pre zero)       : refl _
                            ...   = prim_rec_fun x f zero zero             : { pre_zero }
                            ...   = simp_rec (λ n, x) faux zero zero       : refl _
-                           ...   = x                                      : congr1 zero Heq1,
+                           ...   = x                                      : congr1 Heq1 zero,
    have Hs : ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m,
      from take m,
         have Heq1 : pre (succ m) = m,
@@ -456,7 +456,7 @@ theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A)
         calc prim_rec x f (succ m) = prim_rec_fun x f (succ m) (pre (succ m)) : refl _
                               ...  = prim_rec_fun x f (succ m) m              : congr2 (prim_rec_fun x f (succ m)) Heq1
                               ...  = simp_rec (λ n, x) faux (succ m) m        : refl _
-                              ...  = faux (simp_rec (λ n, x) faux m) m        : congr1 m Heq2
+                              ...  = faux (simp_rec (λ n, x) faux m) m        : congr1 Heq2 m
                               ...  = f (prim_rec x f m) m                     : refl _,
    show prim_rec x f zero = x ∧ ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m,
      from and_intro Hz Hs
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index c12e75b9bb..67451cdabf 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean
index 3038a7c20f..d774427e4d 100644
Binary files a/src/builtin/obj/num.olean and b/src/builtin/obj/num.olean differ
diff --git a/src/builtin/obj/optional.olean b/src/builtin/obj/optional.olean
index 12b7fcfd86..d559e0fe1a 100644
Binary files a/src/builtin/obj/optional.olean and b/src/builtin/obj/optional.olean differ
diff --git a/src/builtin/optional.lean b/src/builtin/optional.lean
index 2b37bad164..a61713dfad 100644
--- a/src/builtin/optional.lean
+++ b/src/builtin/optional.lean
@@ -36,14 +36,14 @@ theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a'
    have eq_reps : (λ x, x = a) = (λ x, x = a'),
       from abst_inj (inhab A) (some_pred a) (some_pred a') Heq,
    show a = a',
-      from (congr1 a eq_reps) ◂ (refl a)
+      from (congr1 eq_reps a) ◂ (refl a)
 
 theorem distinct {A : (Type U)} (a : A) : some a ≠ none
 := not_intro (assume N : some a = none,
    have eq_reps : (λ x, x = a) = (λ x, false),
       from abst_inj (inhab A) (some_pred a) (none_pred A) N,
    show false,
-      from (congr1 a eq_reps) ◂ (refl a))
+      from (congr1 eq_reps a) ◂ (refl a))
 
 definition value {A : (Type U)} (n : optional A) (H : is_some n) : A
 := ε (inhabited_ex_intro H) (λ x, some x = n)
diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index 5f73f83194..e6c39a7f21 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -41,6 +41,7 @@ MK_CONSTANT(subst_fn, name("subst"));
 MK_CONSTANT(substp_fn, name("substp"));
 MK_CONSTANT(symm_fn, name("symm"));
 MK_CONSTANT(trans_fn, name("trans"));
+MK_CONSTANT(hcongr1_fn, name("hcongr1"));
 MK_CONSTANT(congr1_fn, name("congr1"));
 MK_CONSTANT(congr2_fn, name("congr2"));
 MK_CONSTANT(congr_fn, name("congr"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index c4de4e3d9d..5fbcfa7258 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -114,6 +114,9 @@ inline expr mk_symm_th(expr const & e1, expr const & e2, expr const & e3, expr c
 expr mk_trans_fn();
 bool is_trans_fn(expr const & e);
 inline expr mk_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_trans_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_hcongr1_fn();
+bool is_hcongr1_fn(expr const & e);
+inline expr mk_hcongr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hcongr1_fn(), e1, e2, e3, e4, e5, e6}); }
 expr mk_congr1_fn();
 bool is_congr1_fn(expr const & e);
 inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); }
diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp
index 6a2ec989d8..c8b9e6aa21 100644
--- a/src/library/simplifier/simplifier.cpp
+++ b/src/library/simplifier/simplifier.cpp
@@ -240,7 +240,7 @@ class simplifier_cell::imp {
     expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) {
         expr const & A = abst_domain(f_type);
         expr B = lower_free_vars(abst_body(f_type), 1, 1);
-        return ::lean::mk_congr1_th(A, B, f, new_f, a, Heq_f);
+        return ::lean::mk_congr1_th(A, B, f, new_f, Heq_f, a);
     }
 
     expr mk_congr2_th(expr const & f_type, expr const & a, expr const & new_a, expr const & f, expr Heq_a) {
diff --git a/tests/lean/add_assoc.lean.expected.out b/tests/lean/add_assoc.lean.expected.out
index 0bf04407ff..aac3b3dad3 100644
--- a/tests/lean/add_assoc.lean.expected.out
+++ b/tests/lean/add_assoc.lean.expected.out
@@ -9,9 +9,9 @@ Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1
 theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c :=
     Nat::induction_on
         a
-        (eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c))) (congr1 c (congr2 Nat::add (Nat::add_zerol b))))
+        (eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c))) (congr1 (congr2 Nat::add (Nat::add_zerol b)) c))
                          (eq_id (b + c))))
         (λ (n : ℕ) (iH : n + (b + c) = n + b + c),
-           eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 1 (congr2 Nat::add iH))))
-                                  (trans (congr1 c (congr2 Nat::add (Nat::add_succl n b))) (Nat::add_succl (n + b) c)))
+           eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 (congr2 Nat::add iH) 1)))
+                                  (trans (congr1 (congr2 Nat::add (Nat::add_succl n b)) c) (Nat::add_succl (n + b) c)))
                            (eq_id (n + b + c + 1))))
diff --git a/tests/lean/bad_simp2.lean.expected.out b/tests/lean/bad_simp2.lean.expected.out
index bf39709a0e..7aef502857 100644
--- a/tests/lean/bad_simp2.lean.expected.out
+++ b/tests/lean/bad_simp2.lean.expected.out
@@ -28,5 +28,5 @@ bad_simp2.lean:51:3: error: failed to create proof for the following proof state
 Proof state:
 A : Type, B : (Type 1) ⊢ h2 A B = A
 theorem T5a (A B : Type) : h2 A B = A :=
-    eqt_elim (trans (congr1 A (congr2 eq (Ax5 A B (eqt_elim (trans (congr1 A (congr2 eq (Ax1 A))) (eq_id A))))))
+    eqt_elim (trans (congr1 (congr2 eq (Ax5 A B (eqt_elim (trans (congr1 (congr2 eq (Ax1 A)) A) (eq_id A))))) A)
                     (eq_id A))
diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out
index a823e00e39..1843bc4dd1 100644
--- a/tests/lean/find.lean.expected.out
+++ b/tests/lean/find.lean.expected.out
@@ -1,7 +1,7 @@
   Set: pp::colors
   Set: pp::unicode
   Imported 'find'
-theorem congr1 {A B : (Type U)} {f g : A → B} (a : A) (H : f = g) : f a = g a
+theorem congr1 {A B : (Type U)} {f g : A → B} (H : f = g) (a : A) : f a = g a
 theorem congr2 {A B : (Type U)} {a b : A} (f : A → B) (H : a = b) : f a = f b
 theorem congr {A B : (Type U)} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
 find.lean:3:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo'
diff --git a/tests/lean/simp10.lean.expected.out b/tests/lean/simp10.lean.expected.out
index 903a56b3b5..9e77039d14 100644
--- a/tests/lean/simp10.lean.expected.out
+++ b/tests/lean/simp10.lean.expected.out
@@ -8,5 +8,5 @@
   Proved: one_neq_0
 a
 fid a
-    (eqt_elim (trans (trans (congr1 0 (congr2 neq (gcnst a))) neq_to_not_eq)
+    (eqt_elim (trans (trans (congr1 (congr2 neq (gcnst a)) 0) neq_to_not_eq)
                      (trans (congr2 not (neq_elim one_neq_0)) not_false)))
diff --git a/tests/lean/simp17.lean.expected.out b/tests/lean/simp17.lean.expected.out
index ce3f0ca925..a3ee66757b 100644
--- a/tests/lean/simp17.lean.expected.out
+++ b/tests/lean/simp17.lean.expected.out
@@ -6,8 +6,8 @@
 ⊥
 trans (and_congrr
            (λ C::1 : b = 0 ∧ c = 1,
-              trans (congr (congr2 neq (congr1 0 (congr2 Nat::add (and_elimr C::1))))
-                           (congr1 1 (congr2 Nat::add (and_eliml C::1))))
+              trans (congr (congr2 neq (congr1 (congr2 Nat::add (and_elimr C::1)) 0))
+                           (congr1 (congr2 Nat::add (and_eliml C::1)) 1))
                     (a_neq_a 1))
            (λ C::7 : ⊥, refl (b = 0 ∧ c = 1)))
       (and_falser (b = 0 ∧ c = 1))
diff --git a/tests/lean/simp24.lean.expected.out b/tests/lean/simp24.lean.expected.out
index 07d65e5757..cb7c4adf30 100644
--- a/tests/lean/simp24.lean.expected.out
+++ b/tests/lean/simp24.lean.expected.out
@@ -9,4 +9,4 @@ funext (λ x : ℕ, trans (imp_congr (refl (x = a)) (λ H : x = a, eq_id x)) (im
 λ x : ℕ, ⊤
 funext (λ x : ℕ, trans (imp_congr (congr2 (eq x) (Nat::add_zeror a)) (λ H : x = a, eq_id a)) (imp_truer (x = a)))
 λ x : ℕ, a = 1 → x > 1
-funext (λ x : ℕ, imp_congr (congr1 1 (congr2 eq (Nat::add_zeror a))) (λ C::2 : a = 1, congr2 (Nat::gt x) C::2))
+funext (λ x : ℕ, imp_congr (congr1 (congr2 eq (Nat::add_zeror a)) 1) (λ C::2 : a = 1, congr2 (Nat::gt x) C::2))
diff --git a/tests/lean/simp26.lean.expected.out b/tests/lean/simp26.lean.expected.out
index 55b376054c..537c2ba9b8 100644
--- a/tests/lean/simp26.lean.expected.out
+++ b/tests/lean/simp26.lean.expected.out
@@ -6,12 +6,12 @@
 λ x : ℕ, a = 1 → x > f (λ y : ℕ, y + 1)
 funext (λ x : ℕ,
           imp_congr
-              (congr1 1 (congr2 eq (Nat::add_zeror a)))
+              (congr1 (congr2 eq (Nat::add_zeror a)) 1)
               (λ C::4 : a = 1, congr2 (Nat::gt x) (congr2 f (funext (λ y : ℕ, congr2 (Nat::add y) C::4)))))
 λ x : ℕ, a = 1 → x = 2 → 2 > f (λ y : ℕ, y + 1 + 2)
 funext (λ x : ℕ,
           imp_congr
-              (congr1 1 (congr2 eq (Nat::add_zeror a)))
+              (congr1 (congr2 eq (Nat::add_zeror a)) 1)
               (λ C::8 : a = 1,
                  imp_congr
                      (refl (x = 2))
diff --git a/tests/lean/simp29.lean.expected.out b/tests/lean/simp29.lean.expected.out
index 26a034e406..7f6ba1e616 100644
--- a/tests/lean/simp29.lean.expected.out
+++ b/tests/lean/simp29.lean.expected.out
@@ -5,4 +5,4 @@
   Assumed: f
   Assumed: fNat
 (∀ x : ℕ, x > 0) ∧ (∀ x : Bool, f x)
-congr1 (∀ x : Bool, f x) (congr2 and (allext (λ x : ℕ, fNat x)))
+congr1 (congr2 and (allext (λ x : ℕ, fNat x))) (∀ x : Bool, f x)
diff --git a/tests/lean/simp3.lean b/tests/lean/simp3.lean
index 6d350997a7..7b6c655193 100644
--- a/tests/lean/simp3.lean
+++ b/tests/lean/simp3.lean
@@ -40,16 +40,16 @@ print(pr)
 *)
 
 theorem congr2_congr1 {A B C : TypeU} {f g : A → B} (h : B → C) (Hfg : f = g) (a : A) :
-        congr2 h (congr1 a Hfg) = congr2 (λ x, h (x a)) Hfg
-:= proof_irrel (congr2 h (congr1 a Hfg)) (congr2 (λ x, h (x a)) Hfg)
+        congr2 h (congr1 Hfg a) = congr2 (λ x, h (x a)) Hfg
+:= proof_irrel (congr2 h (congr1 Hfg a)) (congr2 (λ x, h (x a)) Hfg)
 
 theorem congr2_congr2 {A B C : TypeU} {a b : A} (f : A → B) (h : B → C) (Hab : a = b) :
         congr2 h (congr2 f Hab) = congr2 (λ x, h (f x)) Hab
 := proof_irrel (congr2 h (congr2 f Hab)) (congr2 (λ x, h (f x)) Hab)
 
 theorem congr1_congr2 {A B C : TypeU} {a b : A} (f : A → B → C) (Hab : a = b) (c : B):
-        congr1 c (congr2 f Hab) = congr2 (λ x, f x c) Hab
-:= proof_irrel (congr1 c (congr2 f Hab)) (congr2 (λ x, f x c) Hab)
+        congr1 (congr2 f Hab) c = congr2 (λ x, f x c) Hab
+:= proof_irrel (congr1 (congr2 f Hab) c) (congr2 (λ x, f x c) Hab)
 
 rewrite_set proofsimp
 add_rewrite congr2_congr1 congr2_congr2 congr1_congr2 : proofsimp
diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out
index df175dcbcd..75b88dc898 100644
--- a/tests/lean/simp3.lean.expected.out
+++ b/tests/lean/simp3.lean.expected.out
@@ -20,9 +20,9 @@ trans (Nat::distributel a b (c + d))
   Proved: congr1_congr2
 ⊤
 trans (congr (congr2 eq
-                     (congr1 10
-                             (congr2 Nat::add (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b)))))
-             (congr1 10 (congr2 Nat::add (if_a_a (a > 0) b))))
+                     (congr1 (congr2 Nat::add (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b)))
+                             10))
+             (congr1 (congr2 Nat::add (if_a_a (a > 0) b)) 10))
       (eq_id (b + 10))
 trans (congr (congr2 (λ x : ℕ, eq ((λ x : ℕ, x + 10) x))
                      (trans (congr2 (ite (a > 0) b) (Nat::add_zeror b)) (if_a_a (a > 0) b)))
diff --git a/tests/lean/simp31.lean.expected.out b/tests/lean/simp31.lean.expected.out
index 0cf34d763e..5882fd47be 100644
--- a/tests/lean/simp31.lean.expected.out
+++ b/tests/lean/simp31.lean.expected.out
@@ -38,5 +38,5 @@ Step: a + (a + b) ===> a + (a + b)
 Step: a + (b + a) ===> a + (a + b)
 Step: a + (b + 0) + a ===> a + (a + b)
 a + (a + b)
-trans (trans (congr1 a (congr2 Nat::add (congr2 (Nat::add a) (Nat::add_zeror b)))) (Nat::add_assoc a b a))
+trans (trans (congr1 (congr2 Nat::add (congr2 (Nat::add a) (Nat::add_zeror b))) a) (Nat::add_assoc a b a))
       (congr2 (Nat::add a) (Nat::add_comm b a))
diff --git a/tests/lean/simp33.lean.expected.out b/tests/lean/simp33.lean.expected.out
index 224c905c18..5b2901b12e 100644
--- a/tests/lean/simp33.lean.expected.out
+++ b/tests/lean/simp33.lean.expected.out
@@ -6,4 +6,4 @@
   Assumed: Ax2
   Proved: T1
 theorem T1 (a : ℕ) : f (f a > 0) :=
-    eqt_elim (trans (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥)) not_false)
+    eqt_elim (trans (trans (congr2 f (congr1 (congr2 Nat::gt (Ax2 a)) 0)) (Ax1 ⊥)) not_false)