From a6e0dcc96c53acd45ca4b52eb2ab30495d4eb2e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Jan 2014 16:19:11 -0800
Subject: [PATCH] fix(builtin/cast): remove dominj axiom, it is not consistent
 with the new semantics of Pi/forall

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/cast.lean                      |  78 ++++++++++++++++++---
 src/builtin/kernel.lean                    |  17 ++---
 src/builtin/obj/cast.olean                 | Bin 743 -> 2669 bytes
 src/builtin/obj/kernel.olean               | Bin 15032 -> 14908 bytes
 tests/lean/cast2.lean                      |   5 --
 tests/lean/cast2.lean.expected.out         |   5 --
 tests/lean/cast4.lean                      |  19 +----
 tests/lean/cast4.lean.expected.out         |  18 +----
 tests/lean/eq3.lean                        |   1 +
 tests/lean/eq3.lean.expected.out           |   1 +
 tests/lean/mod1.lean.expected.out          |   4 +-
 tests/lean/norm_bug1.lean                  |   6 +-
 tests/lean/norm_bug1.lean.expected.out     |   9 ++-
 tests/lean/type_inf_bug1.lean              |   5 +-
 tests/lean/type_inf_bug1.lean.expected.out |   9 +--
 15 files changed, 92 insertions(+), 85 deletions(-)

diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean
index 1510e6f83..b4ec39743 100644
--- a/src/builtin/cast.lean
+++ b/src/builtin/cast.lean
@@ -1,24 +1,80 @@
 -- "Type casting" library.
 
+-- Heterogeneous substitution
+axiom hsubst {A B : TypeU} {a : A} {b : B} (P : ∀ (T : TypeU), T -> Bool) : P A a → a == b → P B b
+
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
+
+-- Type equality axiom, if two values are equal, then their types are equal
+theorem type::eq {A B : TypeM} {a : A} {b : B} (H : a == b) : A == B
+:= hsubst (λ (T : TypeU) (x : T), A == T) (refl A) H
+
+-- Heterogenous symmetry
+theorem hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a
+:= hsubst (λ (T : TypeU) (x : T), x == a) (refl a) H
+
+-- Heterogenous transitivity
+theorem htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c
+:= hsubst (λ (T : TypeU) (x : T), a == x) H1 H2
+
 -- The cast operator allows us to cast an element of type A
 -- into B if we provide a proof that types A and B are equal.
-variable cast {A B : (Type U)} : A == B → A → B.
+variable cast {A B : TypeU} : A == B → A → B
 
 -- The CastEq axiom states that for any cast of x is equal to x.
-axiom cast::eq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x.
+axiom cast::eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x
 
 -- The CastApp axiom "propagates" the cast over application
-axiom cast::app {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
-              (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : A == A')
-              (f : ∀ x : A, B x) (x : A) :
-    cast H1 f (cast H2 x) == f x.
+axiom cast::app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU}
+                (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : A == A')
+                (f : ∀ x : A, B x) (x : A) :
+    cast H1 f (cast H2 x) == f x
 
+-- Heterogeneous congruence
+theorem hcongr
+            {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM}
+            {f : ∀ x : A, B x} {g : ∀ x : A', B' x} {a : A} {b : A'}
+            (H1 : f == g)
+            (H2 : a == b)
+         : f a == g b
+:= let L1 : A  == A'                             := type::eq H2,
+       L2 : A' == A                              := symm L1,
+       b' : A                                    := cast L2 b,
+       L3 : b == b'                              := cast::eq L2 b,
+       L4 : a == b'                              := htrans H2 L3,
+       L5 : f a == f b'                          := congr2 f L4,
+       S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm (type::eq H1),
+       g' : (∀ x : A, B x)                      := cast S1 g,
+       L6 : g == g'                              := cast::eq S1 g,
+       L7 : f == g'                              := htrans H1 L6,
+       L8 : f b' == g' b'                        := congr1 b' L7,
+       L9 : f a == g' b'                         := htrans L5 L8,
+      L10 : g' b' == g b                         := cast::app S1 L2 g b
+   in htrans L9 L10
+
+exit -- Stop here, the following axiom is not sound
+
+-- The following axiom is unsound when we treat Pi and
+-- forall as the "same thing". The main problem is the
+-- rule that says (Pi x : A, B) has type Bool if B has type Bool instead of
+-- max(typeof(A), typeof(B))
+--
+-- Here is the problematic axiom
 -- If two (dependent) function spaces are equal, then their domains are equal.
 axiom dominj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
              (H : (∀ x : A, B x) == (∀ x : A', B' x)) :
-    A == A'.
+      A == A'
+
+-- Here is a derivation of false using the dominj axiom
+theorem unsat : false :=
+let L1 : (∀ x : true, true)                         := (λ x : true,  trivial),
+    L2 : (∀ x : false, true)                        := (λ x : false, trivial),
+    -- When we keep Pi/forall as different things, the following two steps can't be used
+    L3 : (∀ x : true, true) = true                  := eqt::intro L1,
+    L4 : (∀ x : false, true) = true                 := eqt::intro L2,
+    L5 : (∀ x : true, true) = (∀ x : false, true)  := trans L3 (symm L4),
+    L6 : true = false                                := dominj L5
+in L6
 
--- If two (dependent) function spaces are equal, then their ranges are equal.
-axiom raninj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
-             (H : (∀ x : A, B x) == (∀ x : A', B' x)) (a : A) :
-    B a == B' (cast (dominj H) a).
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index ba17645ca..3fe4e71cc 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -45,26 +45,23 @@ definition neq {A : TypeU} (a b : A) : Bool
 
 infix 50 ≠ : neq
 
-axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
-
 axiom refl {A : TypeU} (a : A) : a == a
 
 axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b
 
-definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
-:= subst H1 H2
-
-axiom eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
-
 axiom iff::intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a == b
 
 axiom abst {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x == g x) : f == g
 
 axiom abstpi {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x)
 
-axiom hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a
+axiom eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
 
-axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c
+axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
+
+-- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
+definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
+:= subst H1 H2
 
 theorem trivial : true
 := refl true
@@ -189,7 +186,7 @@ theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H :
 -- because the types are not definitionally equal
 
 theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
-:= htrans (congr2 f H2) (congr1 b H1)
+:= subst (congr2 f H2) (congr1 b H1)
 
 -- Remark: the existential is defined as (¬ (forall x : A, ¬ P x))
 
diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean
index f65b61fe786e24f88e0fecad8fb81b521e092bce..5d0d947928165957c9d6a3115c1395776b29138f 100644
GIT binary patch
literal 2669
zcma)8-)j_C6u$Q~nc2;1{hgH78nBwEP%v75u`eb?8!=If=B0>blAXk0vb)`kqOS=e
z5~yIGEGT)9LMfC!`Cy?>`hWF&-<dl%D?T{j-EY2o&bjA&=gf_rl{{-NF0bUSeEjli
zx6>=!y}Z}XS6umaEh}91(8=Ak`}1psOJvfC+<Mf_=bXMwnQtPQ^9p?;^JEm<(Cu6O
z+v+*h>8!vpb4Rcz@EX7(;A%jh=|7ipJH`7T-s@LZyZGfZ;PtuRUVf1G)^aDa&cjX@
zneP-XZp>91aNE(!7adcdb*XuPmXvF8*9}Oab-DZ(s}l6Cs>WgDhi7|@)2>Deix4J&
zb*8)*aF}pkg!=(K*#i*{1CAUQ{MciGfSI2k3}Oz-Ls|&MqM1J;(#scBSUe0%UV><Q
zl%{A}rFQbs>MBd5d0!L3^cM(bBvzR+^RK{KV-806HK3JtD8f;|k>gm&enMfer4$LL
z;2XTt%~}<z`cmmwRng1ZYacD^d-&VX;WrIKs$c;GnCS^?rHQTYr?}IMO|{CIi&f6t
z3?8L1r5R&D!tn@?MMx!@G&lja8Kt3A4Uly#=|_4Fo@UesWACaiAJ&%ypN97jvYwNL
zto&eMRSmKN8|0AySaTXw{Z?(od;R7IEJFD`d>CY!ga)y3OsSNNF)zdjMF92Zd0Lsi
z6S8i1d*dc4oMjwxWCYY;d$+A);qW@!!aDRGDH9@RCs+OaB9TRnVipZr*q0Kx(Hak!
zBYP3vDXmO%vXiK2lq`G2irFyF=Ih1iT#H6nEGwX&gTxo~B@XUFr@hpx>eqXwtY6WT
z(ivP$K`>T-fjaQqNn|MivuuR%R-jXjXQ-;bS&Mm_Xe`NQ`v=(Cg~jF?yaKl1yk3oP
z2JjBq*$A%zHppI&@CM)z*&hL$b(xuPp7&QB64%D5A#N$>*0F40v5x>q)Z>(T0I$Pi
zXiS9H7#O?po&eEVt>?$>>Tkr3aDNj<JS@?Wr^}GmMjKrWr*oS)WCsv{YpC&er7=6}
zPcX<~ZtsN2Gc3PhiLIwE1x5j9Gyv6SCL0l^$3!>;dgs99^Kiw#pbdlaII5E342IC4
zH=$#g-51#To#)*~oLzJ$E7ajB4EX0^3+UxI*2h@3u)M@Vg&4k7mnD@k#@o$!uV7{I
zIO$t>{{sti+|)|XmQqm@GyRoT$P}6FVWiiU6NP%Fp65zWChd7YJ`YZN>GWsi^cT=S
zSZGa|7$}G{b3Q1}oLlry;m`_->-PbdeH_l8u=R#ke*>}}x|$O?P4Yqr%L1%PoYf6W
zI7YBN2HSx5e^}mfpS~pj1!*Iw!6#0J=oEgP9yV=yuD<QZav&!Bj^W<GP9poB>^rhp
x7@xve(%Ukn(d%gcBnEs%$o$Q~!jNSns18N1{t8{z(`xot$oos})@A$`^MCt*!RP=0

literal 743
zcmbVK!A=4}4DFO*SV%mWpeVt_#01Xr2arhc;>{13$daJ2tSd2mzI|_4T(8cd+rDYv
zYrC`G=CN3Bwz-^++w97Hb&!v|D)OzIqL+A(?^ubx#jk?|ok_=uzM3~rbwQ(K&U^=B
zcoaB_z(4Owe0kKlcod(A@=tQ{qCvGJ&<c8_<1>78OfpljpasOkP)=)wjv;>(Vp%pN
zW)sw)zd3t^PX-|A?lS1|QL<XR_kbKqX^nYeN!hZeX>#WDg07A0NY*y<1|VQ9Dndq?
zZUEW`(qYyJu@b$4J0f~Z6s8B`#;{$OI~W$F-VpZdHC$NWogG`XuJ*f4@or7ckb~Kq
zTL5AsH--ly*DyCV-_U|HUlogg@Zm+^3^ESJag?tA9g5=)Cj8OR6iG<?^b!~i+qmEs
Wx!Ng0EK<(T;NAlE`&6tJc-%i_<~UIR

diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 1729d77efadeadb278fac1fdcdd186afdaa2925e..6a147dec0f1e32e0eeea946bebe92cd9301d518c 100644
GIT binary patch
literal 14908
zcmbVT4UnBxdH&A1cW*8~n_^mnCeb9ohOITt5V~Z8SWQ~UMt4MIDU4-C?<RM1Z@al0
z_9rB5q)P2b@TVFbf7?RG5&VJvP-;V~)dZyukxD70k=hnRQf*|W*j9o%Lf_|kzVn@P
zzr9JIJCn2TIp;m^|NEYwZ!<O7Y;-2tlg%vuadVya&gS$?GxJwx&e^Cnetc>++u4}T
z{Kl!N$!r0JZDM?`JvrO%WR=<Jxn@@MCK{8ryy&(kvd!CfWZr&bk=xpw$o$yu9nGta
zP|g4|*#a~bPIru7%{MZSAvRg94{(hQrX&NV-!L`Xm~BsWFy;KgJMlXk<f^`m<ff)c
z4dW!RfV9qJzt4~3cUA+@^8uYjp#b%Flisr@tJvtvN&1Yed-A$9n#8(A-BU+y{!B7Q
zi5i`)K+MkWGp_il6>>-hNQ0k#Gz+<=y?w`IyE%h_UhBG6lq6rZiUOQZ$<HZCzUDej
zg6@*C<aZ=<l%lz-Ju^FF_S_)HR1JJ%Vct53$Vs&EGW3@cd>O!HLAzb(W&P^1rKWZ9
zxSsTZu{5YvujP&+o}ytTF-ZM9fOUeRMoB~y;fJ3U_RqO)4PVVbT1&&MP_%TK*8@Ad
zu+MbF&(h$edT>%MHzo%I^#SXYsUO*UTS9*zYwXJWbaP^|hkBG(O`!M+QpB2>x$zlf
zL@v*Kn*<*?TS8qdoJTHFJd@~<_19)~%vbDRHbg580UQqeR$Hg)?8jJEEng?Hc4u~a
zs&KB+9LECWiV?@pxg;Cpp}B`KzCO^r#5$f7eWRqq#)2><G*3_1NFEp<vb^TEDVV5t
zBC-X;NP#=d<s)1nT><t72`;lv(26qbXxq}lk{f}XT~YJDQiww}Oq|Gqc6yz0m2|^2
z9u<vaATtt}UT&R=Ea{uGjh+ly53@}cRH8~I%R#0d$h^Tix%IX*tf<1x_*p;)Pzq}7
z=mz#Fybm5>DvmL!7(+^g*PbG>`*IeS^aUTUGiWW@u2)rE&6w^(ELAZ+95iU5H-?5%
z6lz>+Be2G7EAz9{?Vat$B#<(90b><$o>vW`G`AP7s9k`mMQG|&?<|7MbH-wA6-iu`
z1sSOE90%V9+-x_Ry0NZ$?M%(dcESK|#t&EYlQ12l3bTz<tI*!i#errQX-xJ*H4E^$
z>8(+AItjA~S6Of&x}IEq1E9G4CO{Q08fIbiY!Sw7Ly-lW*IPX+96UcK2McbDs3CIW
z?kH|k;3kmaFh~T}yrDtNQEA$dAx<hcVuDH+5^c8;3(oF(df6UYax2Zby|mLD`RGlW
z1+jf}N!xUpoo;lnqckv#;xZn9Edj{O&E7&agM<#dSOlWoiAIXu5J4uFM(MA;#QiNG
z?6t_wsl?nVa(K=#@~Ev^IW$3SWBC8bItpGNBHMQWlrZm%;7t+yU4RntT>wX;h>XI0
z7?jR{m}iB=zhfg&Vw3iTS(kEtm~!p~amjg01m6?E_X31)itBlnjKa2nNr@RqMNzof
zhNG|@JMrP42^~CJOEP{IM3f=4K&?kg-U}SMSb2%~s``R(&#d2%HOl&r0+h-h1Grx*
zFfdqkn7jQtLwyh!r7HIk8&QUC*Xb1~X*753nV3|blei-I6I?<Md@_Q60PtLn{vp7H
zMNAA2Fwbb+jLA9zgd#;hZXHWe6sIjywwE_{OzHgiKseIGbEgr-T4Ur#I?BL>Dz2bn
zIfjNV>@M!N+OT+3Lj^2X*dm{E3-mLMqh(1|b?SC-kr(cW;Aa5JO`ipLSQ|$Za5gl6
z_7ED%*e%|tZI~9wV}W^Wv4At!{DL#mX^iK$0MI)ZjRd<3palDq2>vO+qml;xH|#Tf
ztFg2B*5<Aq)0vAp9)?-P@UR39{3-PC8Cd*h4(;*iUpW9eq*-4_S87IRbAHOb(}r??
zDEfoO$t5T$v2yxR&{^1r_OH-L(ftv;7vND7Oup=w3K%@zTXIZE#C$%Q;&_}3LVv-A
z@<5$#&P+}2Y+lscKNn^3L=Y|TElU0+(3RwW8^JFd=)6g;N_7}B%LCspTBitJyOW*v
zz^l*&jeZKU1Ry=AFu4zX$?(+(ehr}F_kMvqTq+#6`u=E8_Nm*tAm%|^l!}Q2J4pb`
zJ`^k3N3t<RB-=M2g}?_5a*I_+5IcF2v)UEK`T-j*3vh~fa*IJn3O@u;to|W_4;$zf
z(}dr{XukwN9P||6n>HK-u<Jbi)MWw1v7NN?ViUte+YTe-pFmx*JPJ@d%0Fu~oOchi
z@P8kJ(G?;R{PBp*si^oM46ISqxuUR0Duv1-P^3@fj(<U4!hAb|{|d0*!c`Y6Z90MP
zV>TE0p0vzv0ge2YR<eWQx2yEvYIreMFfp|geTNiiv?CFGB7#Q^bnA(54B({%zYB!p
z(XDnhkO`9bZYKq!&8pC!jI>npzQ{X94dhyALVYAYc1*XCZekp51V-Cf(e932UPJ1b
zC^x~FkK0_hmDr_xZWi~e#B-s;vxf&I1vDc=etXge-I#7gj{`&gO-~9U7#*sljQ*vq
z=yZlyQJLTi?c6iFx8uIDf%JR4hnV{~HAqF10Q&)k_4xAN02S^315ld$FTlY;v^?{x
zj-jjhw*u7lnzV;0>@-KwbSK4AHWKU^j>)GGT0x57Q>2gbPyn){WYz|#OnDlh6gdG<
ziaY~Qg8m4gaDNPNl)?BDf>FH|`qGi}RIf#5oFXLugc$jut>EK9_bunhdu~pyIX}#J
zmFYCI=i{mYNI{ipKJkl#Ny(v*&jFpfJ3!Li5vJ}Ak?C$^K#|HTft65EhAFGyqVzCM
zw4%sAYjg2LZYOcm=mk2mB!M)fW21(0ECkUhg0`RoqRZU^%u8*$g)Voj6H@z3AkgKG
z<=}m=mOC5G`v)<{h$dNT*~WY(mlv|ARFHv8ftuoe513p@fn>`(A{<H*BO<?EG}Bw*
z^9=Wbe;$qCr^3t`dN8q)&AQ+3LwgP|WtA5JlvT8`5aDMrDy#gQLGCt=z8K&i_p*v|
zrl(bC0Gg&NCEU*#vBChpdA;4)=3TA0j7<`#FR_K%@7zlv(4Vt_@589DqVZv5l~T@-
z((d2^9Ln=e5Zvb-*+#H9t8)=WcQnE>jIwOImk~iJaS7m@S5cL@Y`1mSa#rF6{!494
zmD%o8+oo|)-9R*}&D?tMnmECcO?bh?&*re142Nnxs@tuCi#e)fp{y&hMt(jI;1wJt
z)+T~1#G45Y0D+sfqd`Zt9bIc;?ZQ;n;<^?<+Jr2J`aDP6HzY?4w{<G=T*Ofr!yVxA
zV1gCa3o(G3<+kayJ+08dDunhp0W0>h%he?-(B67gC8!8~1s2H)zW`8HV0Nemtj4Ht
ze-Yr-G{_o&ql4DC2LMvfpmc5$DNT!0$C0wqz<1xm@=zY#&s(Qk>7F{D!t=61+mzRq
zx1N;|O!8<bM0F2R6^5TIz!RD*@Jm>sIG_fK0|v6<U>y)x@ErB#G0m;VDD9GMgLhT@
z^r}wAASTAFlkOQ>NocfEouOrhaE7@65(@EIlEe0qMi{!Jn=e~|0S7D(D5<cD{19BQ
zO%0zRLXzu?Q(k2@aIK}<8wo56IcE<oW>ww9k)akCXiDeZ5O-sk%VWYIcNzLJ^s50b
zqxpXspi0JT4D!4nyVn9dN1Sj<LkRje6DZy6m3iEr4w2xm0;|O|eb^v(2z?w}@!K6@
z5K<~;K^>#YhhUpm*+|%;ef}vf6u|kGDbkPhv*n=gNib2Jb5eaX7)tfm0aTW~9^i7;
z#!ym}s!%K&8$f%A<w8`^CzEh}b(?G?xx8(e;(=Du#RoE|>pX3+2sETV?M7eA5pTj2
zpa0z77{ud`zc`rC4`S>Z;K=>xGTH1iOP+N@x@zJs6=DDo5SVY_F8T;Y^D{1>aF_8H
zM<())O)9%06CQ0m6On?@G?4}0to)@Ui-x)m@fc|r%Ervh)D|l)Wee5(79eM}dSRuU
zZ_%f`_S|7u?k&V6`0Ek8jv!)?2J|B}4B+6D9kzdVr&Bok5vdtTC+>}F?zc7mN~|uF
z_g6*(v2F|toiW0oX-A?$2<xSB8!;v8v^azAn@uhi&|yx)wo1EJL|2)@8hA_Aims5H
z!11pMT5gWALO-{@B&*iYhfq)gN&>i#68K*;2vtB4=GJ%9%!bM|SuKi?NVU2&T8662
z6e{RoQrII=P{BkT(DY3p>Wdd%Cz3BxF>Vxbbz=5e>u9-{SAIrQc`VFCjTrK=0SQK$
zdrNN8tRDSAJaWMovMOFn_z^C7x+%-V%|Qp-4rEAV+S4V|o{~&lSTLkG%4gM-c*lkx
zL8-T(zDv;Lkt-2YGD;e2-7LTw<#{_nYy7*>NMvpnj#;A3uYNvAxa~lWuEO8Z^tOy6
z9vU5HZva>m*`?X}>8DBm0nF7`p#_@%FreK<Qv?RM^;VA#BTI4nZ7eRU_i-B&FNc`*
zw*W~irQA*oB+51BW|O}qAm$t}#N$SQ{M_q51aJ=3!d(kc65~&1PPKFBF>whOpwZ^_
zPJr4uZXyV~Xy;gLkiR{T1-Dq&frCKGH(l)$-{eTKn^@4$`#f64O@`GEnErNf@Sg*$
zMa+iJqtD<}DdFH<r9nm>^qilwQ7;-!`GE*a^J72yA-etk5)Y+D5&Kb0PH2_{3NfDN
zKD2~2ixMVg>K=59`;4}GFBr%j?~CC32^OC5aDu-tm((AOlCr!Vh<c%~??3)7gWQ?u
zOOv>$>;)|{ME`YCf@{*1f$x0<iF~%`=O@Q*Is5@ISM7r^^Sm$NBN9WRFqnU+FniC$
zi~*opKyxxvk^=b{sRsofivrRn`NB~AqB_Ye2<+~XWL`m{B%&pD*1C@YESHEUY|Kk0
zm8y3DOSk>J0`B8T%<$g3LsXu*r{m2hu{2TsN%ZldhrgdJe5-)q!jKzTz9qyMr3r*n
zXir(@RY=MrOfj_9-3G9%{?j(*B^4O?{{WI!szQDO14(%+{{e}1oTxmv87coMtW1>W
z<*QKsStzehqB{LBAgLqYrWK{JCTTD?-ARli92y7T)cH4`x<;P`W()`_r|<!e{@x}*
z;yf`U66)Rjqi$T3e<fN3CX`{8p?@d(sw7m7wn+X+Clc_t)6FD63ob<D1C^Viou;wX
zWYEGtQJ_{>ONgKBohM)UbX<8h$dy-OjAtNyl!eyice8Qe@UsnmR~8l&c`(=KS$7X{
zXoA0t;1{@n((Q}d9Kh%WN<BI|-LJxx@-GZ2T+ZM$JEEP^9ZDSrW#W!|qbz?-Fj#6A
zdR;cYn0k@G>D=*w0`-Nu<K1!P^KpkMeHw49DF~+CfQ9oYJQ%_I46Ljvd4o5#%H{IL
zejxYq##d}O^#=Y5vxhsddNof1dFoo<-H%bF#NQF@?E@VkfY48nPUsJ~-8n%7CM@4m
z<pmC&HYte3gx6BKp}dq*pr+)1s$kll+7G$bhq;hh@b>_vHIHfnAHwMBk_)m?8?3bC
zg0BIimkS=W;Vu{Ce|LQnHyn+D!2+xD^p7AeQ63=}?Ax6WfhO%T6e+QPk~$UE&@IVd
zA+S$pp4K;zXiwxuFO^pUCn;F%+zO|0Pht%oZS-WuyO*r-Z=fsi-vJ&i`)IEXR&J4x
z9tK7)AAQ?~Qy=jSx<{gf_r5_Ilu;vzj)1Vlcp`#F0rG>W`)M(%k4822(G*8EZW-}?
z_&YY2%T%@RB3aMpxxVD#l22LLK#=h&Zuj~7T)5E<gX0)n)oWse8Sp*e^b!0|fO^3@
z4sd{@-v@Zrpf&EN)Z^tCAZeO_8dmPWAf_vSgyuHvBRSIx86lV103KG*@{^G$STA3J
ziQ>8ZyBH5|xI7I^O*bZSn%n@qELtM&zuBg!seLlvMMP%R3M%px7ZUsdz-82_xN=wS
z*4`JMDU(0bUt!pldw6woaFjiuW8_}l`Yz`PZ;aB6JeNmJ(XZ?;Btp#UGa>D@AIq1M
z_W^=Tt!aRqzb96>2^k^JqOv9OP^jD;&0w!eGJ_uKdDfEKp8<Wj{YL=h_8%Kmxf=pz
z@g$IK#^?h|s{g`V62*nbPS|joRLOt!z>0Yei$c;oUjoufI)|rGiS`^u%YJ%Pe!|pw
zXjYaCrg_?OWwc!`&uMJ;Xz)JrwDNVx<11i7d3+ThO~r$B<<ZnsQKM*f;E&k9%HuL0
z3qud{dE`hiUoPrgXJTq{Yu6V-K4oY2*`fi${62x-m18sk4yo>76vJLI<$e9>#gYNw
z@;#gHb#-)EkH)Ac&#ZjQ_Y4&2$(@(M&2+9DV>-K6VKJ+K(w7-!Hzd9-@p+MqvN0yv
zHDvutENP)(hQ#jxl@n2Zs-nu#qF6kmw1^Nj(03(j09_nEA@ISca>8yRRzU5iasq7q
zrHmKyZ9^J<+!q0A-v%3IuG<LIgf``jmDO#`E$TLw<zdiL9x$rf|0o#gG&8DALy*1H
zrcmpE#r%GbRfL~8#JWm(h7el*a|MM|U<k>qCByIsyZ#KU=>G1d7+PD@&Gge(5<`Xg
z)6YCHic8AU?Ru@FMkB_zax0|vcox&AFn=yU#n4LtDu!NaP*oXyje+i<H5F9m%B|MK
z&j5}OH&w=DbWo;0`6`7kF6L{oy7JV8XmNGMhcN}eJ{QE$NngPYugdbFfCJqsYf2Hx
z_`b%NuC9VZC=gvyb=K7%q4>|2yhN)=)adt6DgBFWT~9Zi%1h+H1Y*z}gDf&G<yG1;
z&^1bz@m$XL%1XXK?;Dk4j5!8OlEnGrmuU>us>_4~apxoD7eK$#=A657hy8cUylkn1
WJzJ37js)P=>MrkWy#oJZ^#1^biSDrg

literal 15032
zcmbVT4UnBxdH&A1Ke-5-npB#SL^rT*SVe{=ZkRE3A%Tj!s|8Y{#nw)^+1yPoY<83V
zi2=cu25>E-6<Z}$+Yy`sYH6$eWzgbOtAVkl5>uzNX(gpihlaKqTN*92@AEw0Ip@3I
z-c8h<*|YEYd;j0}{Czt$(P~bPw<lUz{^RB*+xuG6Gp)?OHFM5dt?=8YX0v_G>C9g-
zH8qhfL9=yipKDLdwkNa7?DSkKi?#9QgiVjt_INh3dr#)=FDAJit?|rny=hPDt%fKk
zfSzm#iVC|Yjb7b1Gmj<~S-l3h&H`QH0o_+m%{FJ-Q<La&{?C60f3pG3s%1nsHBD@2
zCxRu!^%B-=emnkVbs+5nbT*j+)YFOjmRqulwZ4L=&&oPG-*JgLF>iTi*RlBr3w`9M
zIk^J^vvX=j6+iXJhj;)t_~}8hlylm<_e``~Gic~GuVY4u^R;WqKp#1OX^Hbo-l0z5
zU0LS*fkGd-Xzg#$%+8oTH_I?p1FwzhZ2*akL>;e2eHFo%16&=X+mBk-qbf^E+7OMs
z#E%iHf>@1uZYYkEH=NHA#C`$520>vXC&CH$!_OM~b*@vwAv)4}DrSwmWwNywqq7TZ
zCL?}U1tT?rk#fG#IS{b-TcwQs*n2--z~7%W_h){rY0&|l;b%$R53iHkkzr@`^{SJ1
zAH=WsIU8QVoCdH=x5g*BD2Yf^1imh@Db8We%-r@F#8oa;K%F!jED2K7hy_IldqZT8
z_y@tt5OqBSa4^tYZ<VUEADWUhrT#abMxV7@AD7iY5I>h21XNkJNwK`1nyi7hDw+pt
zUQRTE+6EMz=H6&672^Y<w`Q9~!LP7N6EiZ(Voo-0ExAvkxz|jsDuwIi&>-OzR`bML
zwX8OtwI^q%ry@qv*>(&^M#*JaLA3>v<dW*!6fllPjJ{d25r}2kTfiZHw$}a5$ZA3T
zX2jvxK1ivyVSFz^3egj&!S!e%Xa@B5v~6niib(OwC=*#WEhQ4f*fgrr62;ljQQH>C
zU1#Ki9d^y!w0rkLVlm2lg7OR)2LIUr1t0@M0V7No1=uw^-JDcH!gxa^0Svej4Jn0~
z_sTK`jIj&;EO#3-NbWX9g0M&y3GTE?9X{>c?5@nuPPg~9n-fIgUg_}{QI=;u4rxJ3
zxmf*`=vt1V!FV~FAam6;!1`LEcy$(hjtTU3HY#-HIm1X-y;j%OM7uyB=!!FXh<G0n
z6MQE?zZT`49TX_2P@}U4qM19)P47s&M+L#bq@bl3?1}njfXc=10;mLh3&5oml_a9$
z-DK_3U~8}C<fx!vmlQDrks2Lsh}7N<yrTAt3H&910~~N0z@Y(@!zidnB`Q?khoY0C
zTdl=HxpPf;{VmLXJE+cEORMFvdwyBHKz1)p(l%Lw6Xqr_NF+~7q8*H)8KmKKwn2(;
zC(ug9_atyWf$s%)kYj&EpdZe$P~(i07<+fv5X2t%v}9$B+T!-Z@JcD}BiRpttXRA|
zfgeoZuK^T`zYcKBQhClIz3^T%N@hTv9RI4dB#w>SA56RC^AqIrH-KDxek6e(P2k4>
zf;sv1!NjICnV97gqm+O-jgW{AS|u?%X}ebZ8q>kD^+LoS;8e19AHX{CcZTF4bkN!?
z8nRnN+%@XIf;o!%2LMXs2LXOXB2XM=9mZ~t_JK4*Y0bRfCMiO9YX=T2i>_$sRGbsJ
zJor<bLNPy`K<>&{u=OEMi^?ACXPhB7*rJYt3s+1UpR^VWQ6#6aDO+iqd#1Dp{@buE
zOM7QS3Iy2-117f<T&m;>EIE2DhNwn6{+?AtqZ%?`Il~HD3S%r#`A&_(7xL5}1GlX3
zCkgyhfHKp=0FP_om;;;*^`m?W1y#V9i0u85HHR36FEEbH7qA0VV0D;ivbjA!$pGI9
z6iT3<2Pnq=EP;;#JSlEqe;a+4-__jL+Sb~?XF7AqdyYe`B6wU32l`}s@GMOJf<t*K
z*;fXD48^E#peivF6yoZ0)|A_$>WdN=4swMQE2EzTo~3j#hJ*w?gjRu%0X%7p$(B7y
z=cl@Jj`3nK?@y{YmHGnHU$&;)QKwroQxp4I>$=-#U6ytPNdx~%&i@j4#qM7v@CgIm
zGUHsC>Nt9O1KqD$B|5L2E6=zcmFogW4;fhrkQS7i97bI{d_93j0Lp*=Mj*F?atF>n
zk`&51WxG7E`J_!MvWWm&#DS$BvX%5B-u@1x#oON}@Th^VUx@_1V=jz>*)B#AqN~in
zY5d7i8VUSOU=!7+6L`!(*H0BbkJcVB06*x;z&~1ZV8E^<Xr~Sh$d7HOl_#6zCKN}z
ztA7S|@$xSK)k>GJM3`@9kFQ17cTpr$2uZNVGuEf1;sZ0#M$B_EED|2D<gT)uAPSk|
z-vEl46A63{U{7R5i%y{Xto0?ji>BEz;K<KVB|XT0J5moe@~`C#2Bub`ZxI8->e~rq
znh?w1u~s+C0sjSXgdlBsDw)*|no>c*zefuRW0YB;r_eH@l=oGhSnD7?f+FO{m_^(c
znh7rDwqV4lk)qyJ-GH`6w<0L>Kdm$0fZ$4CZWdPy1<QrX0U+@x<j~&(C?))_L2gWE
zY@o9tD2h9Uy=W*HR6&{SOI^|abg`J3;D1`V%f~*kNYQ4Ybmu^U7e$V2rmL2q{eb}t
zp(W_jBqeD!qeq8cq8ubcx3LvPhvSn{&{^0D6GJ*F#t@{W?;?k^qc~gwq>MX9dgkhK
z*P*DBw5=RVe9H^S5j~AmM~H%5LPq4dfgQ&2sC#wCE$6Yj=F=I)2Jsv+*~%8ta|mmm
zs{27;9SW%sP$M-K@&$;yA3?w5eknl7y$m3=?~oImZDTF<5X)=ORluU~U`SB+`7VIO
zIV@yo2cJvZY1>AdL}#>6=UKkQfh6QsElHR*^4bDW7c_u+C^olE68py?ki<R@pv30#
z#4PAmS)=<9r>zF~;cg}$MSmufM_v@?w7XP+gy7zXk%=McGI+#~Ssy(jKO3})N4iD*
zxQmu3HgT7=L<<(Q1fK4pcxw#Io#A|d(#iz@r4<@mT0s!H2RRM$x=(h~ik6YCT3IY4
zdJS1rfN$-!1J{Cc5jD!f+31`%(r40huL464GyC3)0UDK*&tPZpvxk`Gg9R?c1RkkL
zeZhWf7#On#CkY3YK&^`W#T=kjf_hfYbuoQ#+PqcQ6PMTv^e?hDrByo+?VQFgb2Ep<
zyRXjcLiAl9R)WE>ppWTjD(8~fFi>WsZ^-+}!CNQ+SJ<rtIqiCaT&1|;x=Vo}UrRO`
zTl-PZMu<I`Q$APoyU^*rE<TdGU9RlSNo<8O++!FVGsRC>CHMf2g*&I$chy1@vocG2
z+Sb@MVVo^Dmb5^950WH7dGJPzl@@*yptSIMfKn3!M`JHT>y1>%<p7!X-ID+*c@R2R
ziG=2S%DAm8G{(E9F+B?XI;(UF-Bo5u$cti3FIrw&7&YN(;A|5!BSz)k5LtCcD9RP+
zlLoE?C=L7+K>5KN0Ll-p0w_OtBS0oR$6(k*WJEspYLCvHJfSN6QSSnw5RU=wzmwCT
z(H-Fq#l4Q9ss}tcy{}=MZX+3R(zCTm?F~(Xzi5=_;!ReP%Z1AZ2b6W*^XBob*RDLl
zpx4w99&c8Mt7hE_=md?mAgrv^?t;Kmyl@oN@@9b2@lOL>&DN^{DqCD*kUy8L*8*H2
zO5EMsKHUEdhGxh6Q9c#ODd=!D;SO`^R&<Z7MG3cZJmq1-i57R5{zv680H{laLP$Gr
zvT<Q`_W3hl$bAbn(*#;X9`R?r!0%s%Hd%-~U5C0ve>*^l{&N5oU_TGAmuWF%6GbTm
z%Qi@4dWx{3m0X8or~6rJDIB`SruhCK?$WIZ#C6N4gXO>>@yX-$sLK$X#cMnFMQe1+
ztneFy3YQI_jnT)r1|M#d6}C!-fE&^g@maLyiU5QG%(LMP`3zd~eJh}F2Jssc5n0DN
z6=R7AcQu{~iHuM+i3IPOv|^|S1ctbSw1Z%CW@c*4@=94lVFOWbL@niXW1alkH3e9@
z0Z65_8xuG|5I#r+`fKWFI0waX`?a%}+{IrbF%#;7dDEODHpjmWv!n3-ZAn3l??DZx
zkI-pG6H*Nb^Cj^pd`jA3l4zj%cH>LAbCBK8t*6J1q~XMd;k4Em05hi*G==!Y7=Kle
z^4i2J<a5I%UNwg{gn(jD9Bc+6aNvKz3S<GLbT{0IGaD-7B-_y?ic)P(no)j?%<Hy3
z>Z2f_oQb{$oSqiuwKZ=Q3NJ~?ZxmhBl=hD|L4*`n{$|u6G5-3SlSFj+Q~-r*v&aYQ
zAS3f}9I4=Cs|tSjcviS_Df7goNj$w9v<o~PKt1wwpu`g=MuM(w>?oc+b$SAmqa9J{
z&ZzHTv~W39U{pL3Ma@cgJHR^mxr3k;{{1M#G8YTC4PCkcXz=>q-O83|DtyD!T{8{?
zsYjkh-Fr~43++W&U-3!N-@~zMQQm34{-c2AW6?payLcjm8KQO<z_NHBw>Hso(67JS
zikw9W2jbQe)H&Onn=QQ1lLqxB8qk(WWQG3-z}t~6+)jW(fzNeLw{qwba3v?8(Beg|
zlmkDA*5pmRTl5d*PV4%05_l4Ww0!031a1s-$B}bs`FN__975$GXx@J&O=1Lp7In^-
z3$pPKON~?&<ZLg9*(4Vgr}&_ylSKYe;EVC`Xo-fnk3pK)WQTf*AhPj&u0tzfwTv86
zIHBrnbp16O<35IwGRJQw@V5wpAuUOd8RQ=i3Vkeb%Jg<9$;A|^^aowK^MFX?(<Jf4
zNwk6{fy5KBu{bl(eLSMbdt*J{HFWaf4}mx@aXgsGZ+0RHPAU!}Gf`pw8&T~@0}BE(
zIe>CO%_z7}fKI^yo<==7z|)CA>Lj12l%6$`IE7vynD5|ZK|&%YDIv)fAH>9Rig?!A
zym(To`T$1p^kAQ1Ac?yB*pec=`|6N{XXfQm!+jc43&QhK*$3;LOp2#?O4-5t^Ccnq
zXkkp0p1gE7gs_1D@$&oRWxz^z2SN0_fI?g`uRVtz&6Mz;LPH_Fl|TH@ij#!rVj_Zn
zfSF173f#eXk!>qA2(PD1?SANxlo9uPxtFG#q{h=LM`NfQyaw`n)56O-9fHEieK1Df
z$rJ{$pCi*C<hzAi-83nG-B}L4$-@E2>OP0MGRfx&!kr5r*CYh~A)1*8sKKRSDEB;B
z;rjspY#ds_!6M`Mc|a@}Ga#~X<_l@&k9M1hHtvD+m<p-OS7zHWhR-edTRAsk<i=dj
zs_si1Llyi*0>8`&l<VF;G-I31WK+3Fq4x+{^PB`I-e`Q$D&cSjquCbiwC2zWjZRrG
z2U2!!j>icG9qX>8sN;>4iwMqSj(g(JAJiQ0Pcy$CbC}R)u*RhkVbL02OJYBnz{3Vs
zE-hJuC$-9(WsO4^+|3$)ZOuh%;M>M7=D_TW8z}S8HOTQvSRwHZbTK_F3<*wS(ZiBP
z=n3}f^lT1Lt_LV9uyGy~SS%709HndrutGDik+WE^T8IirdwM(MQsbnW@9_Qsprqzj
zP2e}tdU44F*_bs}rep#fT)Ud!s5N((Aphoj5i^`jj===0^z=_aE>@l)81&m24*@3?
zF_bW|zDS-5b7+>r*8{B6nA9zcMQj6(?n=~XrSeRSDViqN!Wqm{&<3|Q{1(J<<&!r4
z9e4%)2f&kM8y&R9%H6WjF^uRICOFI$ZN%&6E`buRzVrnvy+#~;8;Hfm$pn4}ARjq>
zHMZ)#sLnbH%0*N2E+Zz=Z&_c?Q`H_NvaZ*2wZg^a7GTTz1CKXwxzF$C!ikQX)eSIJ
zw~lRG2mS|WY6MRK)D7Nu0czL%J%Be1SmCRb;}vKiYN~(|R(=<a=&t-WiU<0v%!yt|
z55dJJE>=)(CWxXi1J$UG=dBX2D!Ch&nr=>DH_5qK(nMOSv#m)|d(c&^P}OTdm0U<t
zPj6ohnbMA{@-TSL&JNd<g?|xPW9^kkcyx0xl--@9<qJCXUB?!l7$q5L_9jVDuRIz#
zT5DCk5K?-cyLw3*`CAvQ*=+#X{|I(XTKC7LgglDMn#f(D@^Dgv-6}~9`p}#%N3;6|
z@YC%6EPyn-e~Cer{8dfbK;QLf{hEU6|IkqI;$Sh}$`^yG@NXuVvA|%7Nvh{d7<4}E
z#6?N0@#(s3r=y9p3pfj?3JOy{b$Nc$UCz%LbaymZA8}fFg8Xpp5kD^jC8_FM3^)o~
zX8EQmNtD!%?rrv4(Z_<GuF*|>*kA_r<*d$4j!#YO=y)7d5ZSXu6NuyGeB}gH037b|
z#76uF3w=(pvLAESp%_I$7hpcxKsmXo;$6O9g?`D2_i!zi{^bT$PB5I^o6yWGpnzu@
zvBTp#)o!N&63R9($i_+fHRu~bK{cdzfXa)B|K}3_{F=uz-HdQRl0c75lmN20!|(}S
z_*7mr+Ll1=r}84m`pxtg(j5gi*|7Zz0i{px`fdx+Y{4MnCZ8#@x-EG;xh*Ar3h!4S
zR9#|BOt!M5@q*Z7>N1Q1`l|kUfX^J_s(Ow!XG3r;|CxxP$S`^;7$he1_Z@#8+QYlH
z-o4~Q>to(5K7AE@D5}5s%#*yhB&?EuQV<>d{u-z=9^^w8f<gJv06->4|0;v3eQ4lA
zi^G1u!fb!PLA-vT<2YWRRF|PK87R}IS|#_zoyB?#tUM2*l@|cp!<bT^o(q!e<j;y2
zgGH=50O_<;0dEx?f)9Bz-q#3KxgR7$G(}bN)0m$vS&42VR+HUhrsR}vW;&gfNPz)V
zH})#n!c_ZeR(eV<mA}^Nxyrddb6?I|u`nS&;-BEkMTaQ_aenz_5(7`QPlHG~MS4Cc
k_#BMo+%<dbUp@1*r3%(;L3TP4fK#h`!{m;u@ZYNc59NgT;s5{u

diff --git a/tests/lean/cast2.lean b/tests/lean/cast2.lean
index 80d8b60ad..14a8242bf 100644
--- a/tests/lean/cast2.lean
+++ b/tests/lean/cast2.lean
@@ -5,8 +5,3 @@ variable A' : Type
 variable B' : Type
 axiom H : (A -> B) = (A' -> B')
 variable a : A
-check dominj H
-theorem BeqB' : B = B' := raninj H a
-set::option pp::implicit true
-print dominj H
-print raninj H a
diff --git a/tests/lean/cast2.lean.expected.out b/tests/lean/cast2.lean.expected.out
index 8ff44375a..7fed7f298 100644
--- a/tests/lean/cast2.lean.expected.out
+++ b/tests/lean/cast2.lean.expected.out
@@ -7,8 +7,3 @@
   Assumed: B'
   Assumed: H
   Assumed: a
-dominj H : A == A'
-  Proved: BeqB'
-  Set: lean::pp::implicit
-@dominj A A' (λ x : A, B) (λ x : A', B') H
-@raninj A A' (λ x : A, B) (λ x : A', B') H a
diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean
index 9496058bc..e06e19615 100644
--- a/tests/lean/cast4.lean
+++ b/tests/lean/cast4.lean
@@ -1,8 +1,5 @@
 import cast
 set::option pp::colors false
-universe M >= 1
-universe U >= M + 1
-definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (B   : A -> TypeM)
@@ -11,20 +8,6 @@ check fun (A A': TypeM)
           (g   : forall x : A', B' x)
           (a   : A)
           (b   : A')
-          (H1  : (forall x : A, B x) == (forall x : A', B' x))
           (H2  : f == g)
           (H3  : a == b),
-    let
-        S1 : (forall x : A', B' x) == (forall x : A, B x) := symm H1,
-        L2 : A' == A                              := dominj S1,
-        b' : A                                    := cast L2 b,
-        L3 : b  == b'                             := cast::eq L2 b,
-        L4 : a == b'                              := htrans H3 L3,
-        L5 : f a == f b'                          := congr2 f L4,
-        g' : (forall x : A, B x)                      := cast S1 g,
-        L6 : g == g'                              := cast::eq S1 g,
-        L7 : f == g'                              := htrans H2 L6,
-        L8 : f b' == g' b'                        := congr1 b' L7,
-        L9 : f a == g' b'                         := htrans L5 L8,
-        L10 : g' b' == g b                        := cast::app S1 L2 g b
-    in htrans L9 L10
+     hcongr H2 H3
diff --git a/tests/lean/cast4.lean.expected.out b/tests/lean/cast4.lean.expected.out
index a162a3574..b17a52c1b 100644
--- a/tests/lean/cast4.lean.expected.out
+++ b/tests/lean/cast4.lean.expected.out
@@ -2,7 +2,6 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
-  Defined: TypeM
 λ (A A' : TypeM)
   (B : A → TypeM)
   (B' : A' → TypeM)
@@ -10,22 +9,9 @@
   (g : ∀ x : A', B' x)
   (a : A)
   (b : A')
-  (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
   (H2 : f == g)
   (H3 : a == b),
-  let S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm H1,
-      L2 : A' == A := dominj S1,
-      b' : A := cast L2 b,
-      L3 : b == b' := cast::eq L2 b,
-      L4 : a == b' := htrans H3 L3,
-      L5 : f a == f b' := congr2 f L4,
-      g' : ∀ x : A, B x := cast S1 g,
-      L6 : g == g' := cast::eq S1 g,
-      L7 : f == g' := htrans H2 L6,
-      L8 : f b' == g' b' := congr1 b' L7,
-      L9 : f a == g' b' := htrans L5 L8,
-      L10 : g' b' == g b := cast::app S1 L2 g b
-  in htrans L9 L10 :
+  hcongr H2 H3 :
     ∀ (A A' : TypeM)
       (B : A → TypeM)
       (B' : A' → TypeM)
@@ -33,4 +19,4 @@
       (g : ∀ x : A', B' x)
       (a : A)
       (b : A'),
-      (∀ x : A, B x) == (∀ x : A', B' x) → f == g → a == b → f a == g b
+      f == g → a == b → f a == g b
diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean
index 9cdb0e399..605b47339 100644
--- a/tests/lean/eq3.lean
+++ b/tests/lean/eq3.lean
@@ -1,3 +1,4 @@
+import cast
 variable Vector : Nat -> Type
 variable n  : Nat
 variable v1 : Vector n
diff --git a/tests/lean/eq3.lean.expected.out b/tests/lean/eq3.lean.expected.out
index 783843fc4..7916c74a6 100644
--- a/tests/lean/eq3.lean.expected.out
+++ b/tests/lean/eq3.lean.expected.out
@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'cast'
   Assumed: Vector
   Assumed: n
   Assumed: v1
diff --git a/tests/lean/mod1.lean.expected.out b/tests/lean/mod1.lean.expected.out
index f9055fbcb..53dcc67b2 100644
--- a/tests/lean/mod1.lean.expected.out
+++ b/tests/lean/mod1.lean.expected.out
@@ -2,5 +2,5 @@
   Set: pp::unicode
   Imported 'cast'
   Imported 'cast'
-@cast : ∀ (A B : (Type U)), A == B → A → B
-@cast : ∀ (A B : (Type U)), A == B → A → B
+@cast : ∀ (A B : TypeU), A == B → A → B
+@cast : ∀ (A B : TypeU), A == B → A → B
diff --git a/tests/lean/norm_bug1.lean b/tests/lean/norm_bug1.lean
index c22faac50..3e4c737bd 100644
--- a/tests/lean/norm_bug1.lean
+++ b/tests/lean/norm_bug1.lean
@@ -1,8 +1,5 @@
 import cast
 set::option pp::colors false
-universe M >= 1
-universe U >= M + 1
-definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (a   : A)
@@ -19,10 +16,9 @@ check fun (A A': TypeM)
           (g   : forall x : A', B' x)
           (a   : A)
           (b   : A')
-          (H1  : (forall x : A, B x) == (forall x : A', B' x))
           (H2  : f == g)
           (H3  : a == b),
-    let L1 : A  == A'               := dominj H1,
+    let L1 : A  == A'               := type::eq H3,
         L2 : A' == A                := symm L1,
         b' : A                      := cast L2 b,
         L3 : b  == b'               := cast::eq L2 b,
diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out
index 05a5fdabc..e44b52a12 100644
--- a/tests/lean/norm_bug1.lean.expected.out
+++ b/tests/lean/norm_bug1.lean.expected.out
@@ -2,7 +2,6 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
-  Defined: TypeM
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
     ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)
@@ -12,10 +11,9 @@
   (g : ∀ x : A', B' x)
   (a : A)
   (b : A')
-  (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
   (H2 : f == g)
   (H3 : a == b),
-  let L1 : A == A' := dominj H1,
+  let L1 : A == A' := type::eq H3,
       L2 : A' == A := symm L1,
       b' : A := cast L2 b,
       L3 : b == b' := cast::eq L2 b,
@@ -29,5 +27,6 @@
       (g : ∀ x : A', B' x)
       (a : A)
       (b : A')
-      (H1 : (∀ x : A, B x) == (∀ x : A', B' x)),
-      f == g → a == b → f a == f (cast (symm (dominj H1)) b)
+      (H2 : f == g)
+      (H3 : a == b),
+      f a == f (cast (symm (type::eq H3)) b)
diff --git a/tests/lean/type_inf_bug1.lean b/tests/lean/type_inf_bug1.lean
index 75458f944..e81e5a60c 100644
--- a/tests/lean/type_inf_bug1.lean
+++ b/tests/lean/type_inf_bug1.lean
@@ -1,8 +1,5 @@
 import cast
 set::option pp::colors false
-universe M >= 1
-universe U >= M + 1
-definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (a   : A)
@@ -22,7 +19,7 @@ check fun (A A': TypeM)
           (H1  : (forall x : A, B x) == (forall x : A', B' x))
           (H2  : f == g)
           (H3  : a == b),
-    let L1 : A  == A'                             := dominj H1,
+    let L1 : A  == A'                             := type::eq H3,
         L2 : A' == A                              := symm L1,
         b' : A                                    := cast L2 b,
         L3 : b  == b'                             := cast::eq L2 b,
diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out
index 0e2af54dc..4bb4b5dba 100644
--- a/tests/lean/type_inf_bug1.lean.expected.out
+++ b/tests/lean/type_inf_bug1.lean.expected.out
@@ -2,7 +2,6 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
-  Defined: TypeM
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
     ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)
@@ -15,7 +14,7 @@
   (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
   (H2 : f == g)
   (H3 : a == b),
-  let L1 : A == A' := dominj H1,
+  let L1 : A == A' := type::eq H3,
       L2 : A' == A := symm L1,
       b' : A := cast L2 b,
       L3 : b == b' := cast::eq L2 b,
@@ -35,5 +34,7 @@
       (g : ∀ x : A', B' x)
       (a : A)
       (b : A')
-      (H1 : (∀ x : A, B x) == (∀ x : A', B' x)),
-      f == g → a == b → f a == cast (symm H1) g (cast (symm (dominj H1)) b)
+      (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
+      (H2 : f == g)
+      (H3 : a == b),
+      f a == cast (symm H1) g (cast (symm (type::eq H3)) b)