Little bit cleaned up

44bcd6f6 · cschoener · b96b1976 · 44bcd6f6
Commit 44bcd6f6 authored 1 year ago by cschoener
--- a/source/casestudies/dhol/dhol.mmt
+++ b/source/casestudies/dhol/dhol.mmt
@@ -217,15 +217,15 @@ theory DHOL : ur:?LF =
 //  isTransRel: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ tm ❙
 //  is_TransRel: {A,r,x,y,z} ⊦isBinRel A r ⟶ x%A ⟶ y%A ⟶ z%A ⟶ ⊦r x y ⟶ ⊦r y z ⟶ ⊦r x z ⟶ ⊦isTransRel A r ❙ 
  isEqRel: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ type ❘ role Judgment ❘
-         = [A,r] {x,y,z,w} x%A ⟶ y%A ⟶ z%A ⟶ w%A ⟶ ⊦(r x x) ∧ (r x w ⇔ r w x) ∧ ((r x y ∧ r y z) ⇒ r x z)❙
+         = [A,r] {x,y,z} x%A ⟶ y%A ⟶ z%A ⟶ ⊦(r x x) ∧ (r x y ⇔ r y x) ∧ ((r x y ∧ r y z) ⇒ r x z)❙

  EqRel_tp: {A,r,x,y} isEqRel A r ⟶ x%A ⟶ y%A ⟶ r x y%bool ❙
  EqRel_refl: {A,r,x} isEqRel A r ⟶ x%A ⟶ ⊦r x x ❘
-            = [A,r,x,P,Q] and_El (and_El (P x x x x Q Q Q Q)) ❙
-  EqRel_sym: {A,r,x,w} isEqRel A r ⟶ x%A ⟶ w%A ⟶ ⊦r x w ⇔ r w x ❘
-           = [A,r,x,w,P,Q,R] and_Er (and_El (P x x x w Q Q Q R)) ❙
+            = [A,r,x,P,Q] and_El (and_El (P x x x Q Q Q)) ❙
+  EqRel_sym: {A,r,x,y} isEqRel A r ⟶ x%A ⟶ y%A ⟶ ⊦r x y ⇔ r y x ❘
+           = [A,r,x,y,P,Q,R] and_Er (and_El (P x y x Q R Q)) ❙
  EqRel_trans: {A,r,x,y,z} isEqRel A r ⟶ x%A ⟶ y%A ⟶ z%A ⟶ ⊦(r x y ∧ r y z) ⇒ r x z ❘
-             = [A,r,x,y,z,P,Q,R,S] and_Er P x y z z Q R S S ❙
+             = [A,r,x,y,z,P,Q,R,S] and_Er P x y z Q R S ❙
                  
  quotient: tp ⟶ (tm ⟶ tm ⟶ tm) ⟶ tp❘# 1 ∕ 2 prec 5❙
  quotient_form: {A,r} isEqRel A r ⟶ $A∕r ❙
@@ -235,17 +235,10 @@ theory DHOL : ur:?LF =

  quotient_E_quick: {A,B,s,t,r} s%A∕r ⟶ ({x} x%A ⟶ (t x) % (B x)) ⟶ ({x,xˈ} x%A ⟶ xˈ%A ⟶ ⊦ (t x) =(B x) (t xˈ)) ⟶ (t s) % (B s) ❘
                  = [A,B,s,t,r,P,Q,R] quotient_E P ([x, u: x%A, v: ⊦ x =(A∕r) s] Q x u) ([x, xˈ, u: x%A, v: xˈ%A, k: ⊦ x =(A∕r) s, l: ⊦ xˈ =(A∕r) s] R x xˈ u v) ❙
-                  
-  app_sub_eq_help: {A,B,f,t,tˈ} t%A ⟶ tˈ%A ⟶ ⊦t =A tˈ ⟶ ({u} u%A ⟶ (f u) % (B u)) ⟶ ⊦ (f t) =(B t) ((λ A [x] f x)@tˈ)❘
-                 = [A,B,f,t,tˈ,P,Q,R,S] eq_trans (S t P) (app_tp (lam_tp eqtp_refl S) P) (wftm_eq (app_tp (lam_tp eqtp_refl S) Q) (dep_type_ext Q P eq_sym R)) (eq_sym (lam_beta ([k,l:k%A] app_tp A B (λ A [x] f x) k (lam_tp eqtp_refl S) l) P)) (app_eq (eq_refl lam_tp eqtp_refl S) R) ❙
-  app_sub_eq_help2: {A,B,f,t,tˈ} t%A ⟶ tˈ%A ⟶ ⊦t =A tˈ ⟶ ({u} u%A ⟶ (f u) % (B u)) ⟶ ⊦ (f tˈ) =(B tˈ) ((λ A [x] f x)@tˈ)❘
-            = [A,B,f,t,tˈ,P,Q,R,S] (eq_sym (lam_beta ([k,l:k%A] app_tp A B (λ A [x] f x) k (lam_tp eqtp_refl S) l) Q)) ❙
+
  app_sub_eq: {A,B,f,t,tˈ} t%A ⟶ tˈ%A ⟶ ⊦t =A tˈ⟶ ({u} u%A ⟶ (f u) % (B t)) ⟶ ⊦(f t) =(B t) (f tˈ)❘   
-            = [A,B,f,t,tˈ,P,Q,R,S] eq_trans (S t P) (app_tp (lam_tp eqtp_refl S) Q) (S tˈ Q) (app_sub_eq_help P Q R S) (eq_sym (app_sub_eq_help2 P Q R S))❙
+            = [A,B,f,t,tˈ,P,Q,R,S] eq_trans (S t P) (app_tp (lam_tp eqtp_refl S) Q) (S tˈ Q) (eq_trans (S t P) (app_tp (lam_tp eqtp_refl S) P) (app_tp (lam_tp eqtp_refl S) Q) (eq_sym (lam_beta ([k,l:k%A] app_tp (lam_tp eqtp_refl S) l) P)) (app_eq (eq_refl lam_tp eqtp_refl S) R)) (lam_beta ([k,l:k%A] app_tp (lam_tp eqtp_refl S) l) Q)❙
            
-  EqRel_subs: {A,r,x,y,z,w} ({s,t} s%A ⟶ t%A ⟶ (r s t)%bool) ⟶ x%A ⟶ y%A ⟶ z%A ⟶ w%A ⟶ ⊦x =A z ⟶ ⊦y =A w ⟶ ⊦(r x y) =bool (r z w) ❘
-            = [A,r,x,y,z,w,P,Q,R,S,T,U,V] (eq_trans bool (r x y) (r x w) (r z w) (P x y Q R) (P x w Q T) (P z w S T) (app_sub_eq A ([m] bool) ([m] r x m) y w R T V ([t,k:t%A] P x t Q k)) (app_sub_eq A ([m] bool) ([m] r m w) x z Q S U ([t,k:t%A] P t w k T)))❙
-
                 
  t_sat_pred: {A,p,s,t} s%A ⟶ t%A ⟶ ⊦s =A t ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ t%(A|p)❘
            = [A,p,s,t,P,Q,R,S,T] refine_I Q valid_eq_flip T (app_sub_eq A ([x] bool) p s t P Q R S)❙
@@ -257,24 +250,15 @@ theory DHOL : ur:?LF =
  t_sat_dep_conj_pred_eq_s: {A,s,t,p} s%A ⟶ t%A ⟶ ⊦s =A t ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦ (((p t) ∧ (t =(A|([x] p x)) s))) ❘
                  = [A,s,t,p,P,Q,R,S,T] refine_E2 (t_sat_pred P Q R ([x,k:x%A] dep_conj_pred_eq_s P S T x k) and_I T (eq_refl (refine_I A ([x] p x) s P T))) ❙                  
  refine_eq_pres: {A,s,t,p} s%A ⟶ t%A ⟶ ⊦s =A t ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦s =(A|p) t ❘
-                = [A,s,t,p,P,Q,R,S,T] (eq_sym and_Er t_sat_dep_conj_pred_eq_s P Q R S T) ❙
-  refine_eq_pres_rev: {A,s,t,p} s%A ⟶ t%A ⟶ ⊦t =A s ⟶ ({x} x%A ⟶ p x % bool) ⟶ ⊦p s ⟶ ⊦t =(A|p) s ❘
-                    = [A,s,t,p,P,Q,R,S,T] eq_sym refine_eq_pres P Q (eq_sym R) S T ❙
-             
+                = [A,s,t,p,P,Q,R,S,T] (eq_sym and_Er t_sat_dep_conj_pred_eq_s P Q R S T) ❙            
     
  eq_conservation_up: {A,B,x,y} x%A ⟶ y%A ⟶ A<B ⟶ ⊦x =A y ⟶ ⊦x =B y ❘
                    = [A,B,x,y,P,Q,R,S] app_sub_eq A ([x] B) ([x] x) x y P Q S ([u,v:u%A] R u v)❙
-                    
-  func_trans_quo: {A,r,x,y,s} $A∕r ⟶ s%A∕r ⟶ x%A ⟶ y%A ⟶ ⊦x =(A∕r) s ⟶ ⊦y =(A∕r) s ⟶ ⊦x =(A∕r) y ❘
-                = [A,r,x,y,s,P,Q,R,S,T,U] eq_trans (quotient_I R P) Q (quotient_I S P) T eq_sym U   ❙
-
-  func_in_quo: {A,B,f,r} $A∕r ⟶ ({x} x%A ⟶ (f x) % B) ⟶ ({x,y} x%A ⟶ y%A ⟶ ⊦x =(A∕r) y ⟶ ⊦(f x) =B (f y)) ⟶ ({x} x%A∕r ⟶ (f x)%B) ❘
-             = [A,B,f,r,P,Q,R] ([s, k:s%A∕r] (quotient_E k ([x, l:x%A, m: ⊦x =(A∕r) s] Q x l) ([x, y, l:x%A, m:y%A, n: ⊦x =(A∕r) s, o: ⊦y =(A∕r) s] R x y l m (func_trans_quo P k l m n o)))) ❙
            
  props_in_true: {F} F%(bool|[x] x =bool true) ⟶ ⊦F ❘
               = [F,P] valid_eq trueI (refine_E2 P)❙                         
  true_props_at_true: {F} F%(bool|[x] x =bool true) ⟶ ⊦F =(bool|[x] x =bool true) true ❘
-                    = [F,P] refine_eq_pres_rev true_tp (refine_E1 P) (refine_E2 P) ([k,l:k%bool] eq_tp l true_tp) (eq_refl true_tp)❙                                      
+                    = [F,P] eq_sym refine_eq_pres true_tp (refine_E1 P) (eq_sym (refine_E2 P)) ([k,l:k%bool] eq_tp l true_tp) (eq_refl true_tp)❙                                      
  props_in_true2: {F} F%bool ⟶ ⊦F ⟶ F%(bool|[x] x =bool true) ❘
               = [F,P,Q] refine_I P (prop_ext F true ([k:⊦F] trueI) ([l:⊦true] Q))❙
  both_true_equals: {F,G} F%bool ⟶ G%bool ⟶ ⊦F ⟶ ⊦G ⟶ ⊦F =(bool|[x] x =bool true) G ❘
@@ -294,15 +278,11 @@ theory DHOL : ur:?LF =
  in_class_quo: {A,r,s} $A∕r ⟶ s%A∕r ⟶ ⊦ ∃ A [y] (y =(A∕r) s) ❘
              = [A,r,s,P,Q] props_in_true (quotient_E_quick Q ([z,k:z%A] in_class_bool_true A r z P k) ([z,zˈ,k:z%A,l:zˈ%A] ground_type_in_class P k l)) ❙

-  prop_quo_true: {A,r,s,p} $A∕r ⟶ s%A∕r ⟶ ({x} x%A ⟶ p x%(bool|[x] x =bool true)) ⟶ (p s)%(bool|[x] x =bool true) ❘
-               = [A,r,s,p,P,Q,R] (quotient_E_quick Q ([z,k:z%A] R z k) ([z,zˈ,k:z%A,l:zˈ%A] both_true_equals (refine_E1 R z k) (refine_E1 R zˈ l) (props_in_true R z k) (props_in_true R zˈ l))) ❙
-
  quotient_triv: {A} isEqRel A ([x,y] x =A y) ❘
-               = [A] [x,y,z,w,k:x%A,l:y%A,m:z%A,n:w%A] and_I (and_I (eq_refl k) (equivalence_I ([u:⊦x =A w] eq_sym u) ([u:⊦w =A x] eq_sym u))) (impl_I ([u:⊦(x =A y)∧(y =A z)] (eq_trans k l m (and_El u) (and_Er u))))❙
-                
+               = [A] [x,y,z,k:x%A,l:y%A,m:z%A,] and_I (and_I (eq_refl k) (equivalence_I ([u:⊦x =A y] eq_sym u) ([u:⊦y =A x] eq_sym u))) (impl_I ([u:⊦(x =A y)∧(y =A z)] (eq_trans k l m (and_El u) (and_Er u))))❙
               
  quotient_sub: {A,Aˈ,r,rˈ} A<Aˈ ⟶ isEqRel A r ⟶ isEqRel Aˈ rˈ ⟶ ({x,y} x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦rˈ x y) ⟶ A∕r < Aˈ∕rˈ ❘
-              = [A,Aˈ,r,rˈ,P,Q,R,S] [s,k:s%A∕r] quotient_E k ([x, l:x%A, m:⊦x=(A∕r) s] quotient_I Aˈ x rˈ (P x l) (quotient_form R)) ([x, xˈ, l:x%A, m:xˈ%A, n:⊦x=(A∕r) s, o:⊦xˈ=(A∕r) s] valid_eq (S x xˈ l m (valid_eq_flip (func_trans_quo A r x xˈ s (quotient_form Q) k l m n o) (quotient_eq l m Q))) (quotient_eq Aˈ x xˈ rˈ (P x l) (P xˈ m) R))❙
+              = [A,Aˈ,r,rˈ,P,Q,R,S] [s,k:s%A∕r] quotient_E k ([x, l:x%A, m:⊦x=(A∕r) s] quotient_I Aˈ x rˈ (P x l) (quotient_form R)) ([x, xˈ, l:x%A, m:xˈ%A, n:⊦x=(A∕r) s, o:⊦xˈ=(A∕r) s] valid_eq (S x xˈ l m (valid_eq_flip (eq_trans (quotient_I l (quotient_form Q)) k (quotient_I m (quotient_form Q)) n eq_sym o) (quotient_eq l m Q))) (quotient_eq Aˈ x xˈ rˈ (P x l) (P xˈ m) R))❙
   
  quotient_subtp: {A,r} $A∕r ⟶ A < A∕r ❘
                = [A,r,P] [x, s: x%A] (quotient_I A x r) s P ❙
@@ -321,11 +301,11 @@ theory DHOL : ur:?LF =
  quotient_eq_triv_quotient: {A} A ≡ A∕([x,y] x=A y) ❘
                           = [A] subtp_antisym (quotient_subtp (quotient_form quotient_triv)) ([s,k:s%A∕([x,y] x=A y)] quotient_E k ([kˈ,l:kˈ%A,m:⊦kˈ =(A∕([x,y] x=A y)) s] l) ([kˈ,lˈ, m:kˈ%A,n:lˈ%A, o:⊦kˈ =(A∕([x,y] x=A y)) s,p:⊦lˈ =(A∕([x,y] x=A y)) s] valid_eq_flip (eq_trans (quotient_I m (quotient_form quotient_triv)) k (quotient_I n (quotient_form quotient_triv)) o (eq_sym p)) quotient_eq m n quotient_triv)) ❙
  quotient_triv_eq: {A,r} isEqRel A r ⟶ isEqRel A ([x,y] x=(A∕r) y) ❘
-                  = [A,r,P] [x,y,z,w, k:x%A,l:y%A,m:z%A,n:w%A] and_I (and_I (eq_refl quotient_I k (quotient_form P)) (equivalence_I ([f:⊦x=(A∕r) w] eq_sym f) ([f:⊦w=(A∕r) x] eq_sym f))) (impl_I ([f:⊦(x=(A∕r) y ∧ y=(A∕r) z)] eq_trans (quotient_I k quotient_form P) (quotient_I l quotient_form P) (quotient_I m quotient_form P) (and_El f) (and_Er f))) ❙
+                  = [A,r,P] [x,y,z, k:x%A,l:y%A,m:z%A] and_I (and_I (eq_refl quotient_I k (quotient_form P)) (equivalence_I ([f:⊦x=(A∕r) y] eq_sym f) ([f:⊦y=(A∕r) x] eq_sym f))) (impl_I ([f:⊦(x=(A∕r) y ∧ y=(A∕r) z)] eq_trans (quotient_I k quotient_form P) (quotient_I l quotient_form P) (quotient_I m quotient_form P) (and_El f) (and_Er f))) ❙
  quotient_triv_eq_eq: {A,r} isEqRel A r ⟶ (A∕r) ≡ A∕([x,y] x=(A∕r) y) ❘
                     = [A,r,P] quotient_eq_rel eqtp_refl P (quotient_triv_eq P) ([x,y, k:x%A,l:y%A] eq_sym quotient_eq k l P ) ❙
  EqRel_on_quo: {A,r} isEqRel A r ⟶ isEqRel (A∕r) r ❘
-              = [A,r,P] [x,y,z,w, k:x%A∕r,l:y%A∕r,m:z%A∕r,n:w%A∕r] and_I (and_I (valid_eq_flip (eq_refl k) (props_in_true (quotient_eqv A x x r k k P ([s,t, f:s%A,g:t%A] EqRel_tp P f g)))) (equivalence_I ([f:⊦r x w]  (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A x w r k n P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A w x r n k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ([f:⊦r w x] (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A w x r n k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x w r k n P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))))) (impl_I ([f:⊦(r x y)∧(r y z)] valid_eq_flip (eq_trans k l m (valid_eq (and_El f) (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h)))) (valid_eq (and_Er f) (props_in_true (quotient_eqv A y z r l m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x z r k m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ❙
+              = [A,r,P] [x,y,z, k:x%A∕r,l:y%A∕r,m:z%A∕r] and_I (and_I (valid_eq_flip (eq_refl k) (props_in_true (quotient_eqv A x x r k k P ([s,t, f:s%A,g:t%A] EqRel_tp P f g)))) (equivalence_I ([f:⊦r x y]  (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A y x r l k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ([f:⊦r y x] (valid_eq_flip (eq_sym (valid_eq f (props_in_true (quotient_eqv A y x r l k P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))))) (impl_I ([f:⊦(r x y)∧(r y z)] valid_eq_flip (eq_trans k l m (valid_eq (and_El f) (props_in_true (quotient_eqv A x y r k l P ([s,t, g:s%A,h:t%A] EqRel_tp P g h)))) (valid_eq (and_Er f) (props_in_true (quotient_eqv A y z r l m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) (props_in_true (quotient_eqv A x z r k m P ([s,t, g:s%A,h:t%A] EqRel_tp P g h))))) ❙
                     
  quotient_idempotent: {A,r} isEqRel A r ⟶ ((A∕r)∕r) ≡ (A∕r) ❘
                     = [A,r,P] subtp_antisym ([s,k:s%(A∕r)∕r] quotient_E k ([x,l:x%A∕r, m:⊦x=((A∕r)∕r)s] l) ([x,y, l:x%A∕r,m:y%A∕r, n:⊦x=((A∕r)∕r)s,o:⊦y=((A∕r)∕r)s] valid_eq (valid_eq_flip (eq_trans (quotient_I (A∕r) x r l (quotient_form (EqRel_on_quo P))) k (quotient_I (A∕r) y r m (quotient_form (EqRel_on_quo P))) n (eq_sym o)) (quotient_eq (A∕r) x y r l m (EqRel_on_quo P))) (props_in_true (quotient_eqv l m P ([z,w, g:z%A,h:w%A] EqRel_tp P g h))))) (quotient_subtp quotient_form EqRel_on_quo P) ❙                     
@@ -334,7 +314,7 @@ theory DHOL : ur:?LF =
              = [A,p,pˈ] subtp_antisym ([k,l:k%(A|p)|pˈ] refine_I (refine_E1 refine_E1 l) (and_I (refine_E2 refine_E1 l) (refine_E2 l))) ([k,l:k%A|([x] p x ∧ pˈ x)] refine_I (refine_I (refine_E1 l) (and_El refine_E2 l)) (and_Er refine_E2 l))❙

  repeated_quo_help: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ isEqRel A rˈ ❘
-                   = [A,r,rˈ,P,Q] [x,y,z,w, k:x%A,l:y%A,m:z%A,n:w%A] and_I (and_I (EqRel_refl Q (quotient_I k (quotient_form P))) (EqRel_sym Q (quotient_I k (quotient_form P)) (quotient_I n (quotient_form P)))) (EqRel_trans Q (quotient_I k (quotient_form P)) (quotient_I l (quotient_form P)) (quotient_I m (quotient_form P)))❙
+                   = [A,r,rˈ,P,Q] [x,y,z, k:x%A,l:y%A,m:z%A] and_I (and_I (EqRel_refl Q (quotient_I k (quotient_form P))) (EqRel_sym Q (quotient_I k (quotient_form P)) (quotient_I l (quotient_form P)))) (EqRel_trans Q (quotient_I k (quotient_form P)) (quotient_I l (quotient_form P)) (quotient_I m (quotient_form P)))❙
  repeated_quo_help2: {A,r,rˈ} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ A∕rˈ < (A∕r)∕rˈ ❘
                    = [A,r,rˈ,P,Q] quotient_sub A (A∕r) rˈ rˈ (quotient_subtp quotient_form P) (repeated_quo_help P Q) Q ([x,y, kˈ:x%A,lˈ:y%A, m:⊦rˈ x y] m )❙
  repeated_quo_help3: {A,r,rˈ,x,y} isEqRel A r ⟶ isEqRel (A∕r) rˈ ⟶ x%A ⟶ y%A ⟶ ⊦r x y ⟶ ⊦rˈ x y ❘
@@ -347,7 +327,7 @@ theory DHOL : ur:?LF =
              = [A,r,rˈ,P,Q] subtp_antisym (subtp_trans (repeated_quo_help5 A r rˈ P Q) (eqtp_subtp (quotient_idempotent (repeated_quo_help A r rˈ P Q)))) (repeated_quo_help2 P Q) ❙
                    
  quo_in_ref_subtp: {A,r,p} isEqRel A r ⟶ ({x} x%A ⟶ p x%bool) ⟶ isEqRel (A|p) r ❘
-                  = [A,r,p,P,Q] [x,y,z,w, k:x%A|p,l:y%A|p,m:z%A|p,n:w%A|p] and_I (and_I (EqRel_refl P (refine_E1 k)) (EqRel_sym P (refine_E1 k) (refine_E1 n))) (EqRel_trans P (refine_E1 k) (refine_E1 l) (refine_E1 m))❙ 
+                  = [A,r,p,P,Q] [x,y,z, k:x%A|p,l:y%A|p,m:z%A|p] and_I (and_I (EqRel_refl P (refine_E1 k)) (EqRel_sym P (refine_E1 k) (refine_E1 l))) (EqRel_trans P (refine_E1 k) (refine_E1 l) (refine_E1 m))❙ 

  repeated_ref_quo_help: {A,r,p} isEqRel A r ⟶ ({x} x%A∕r ⟶ p x%bool) ⟶ (A∕r)|p < (A|p)∕r ❘
                  = [A,r,p,P,Q] ([x,k:x%(A∕r)|p] quotient_E (refine_E1 k) 
@@ -432,23 +412,23 @@ theory DHOL : ur:?LF =
  quo_codomain_EqRel: {A,B,r,x} x%A ⟶ isEqRel (B x) r ⟶ isEqRel ((B x)∕r) r ❘
                    = [A,B,r,x,P,Q] EqRel_on_quo Q ❙
  quo_codomain_EqRel2: {A,B,r} ({x} x%A ⟶ isEqRel (B x) r) ⟶ isEqRel (Π A ([x] (B x)∕r)) ([f,g] ∀ A [x] (r (f@x) (g@x)))❘
-                            = [A,B,r,P] [f,g,h,i, k:f%(Π A ([x] (B x)∕r)),l:g%(Π A ([x] (B x)∕r)),m:h%(Π A ([x] (B x)∕r)),n:i%(Π A ([x] (B x)∕r))] 
+                            = [A,B,r,P] [f,g,h, k:f%(Π A ([x] (B x)∕r)),l:g%(Π A ([x] (B x)∕r)),m:h%(Π A ([x] (B x)∕r))] 
                            (and_I (and_I 
                            (
                            forall_I ([b,c:b%A] EqRel_refl (quo_codomain_EqRel c (P b c)) (app_tp k c))
                            )
                            (
                            equivalence_I 
-                            ([a:⊦∀ A [x] (r (f@x) (i@x))] 
+                            ([a:⊦∀ A [x] (r (f@x) (g@x))] 
                            forall_I ([b, c:b%A]
                            impl_E
-                            (equivalence_El (EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp k c) (app_tp n c)))
+                            (equivalence_El (EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp k c) (app_tp l c)))
                            (forall_E a c)
                            ))
-                            ([a:⊦∀ A [x] (r (i@x) (f@x))] 
+                            ([a:⊦∀ A [x] (r (g@x) (f@x))] 
                            forall_I ([b, c:b%A]
                            impl_E
-                            (equivalence_El (EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp n c) (app_tp k c)))
+                            (equivalence_El (EqRel_sym (quo_codomain_EqRel c (P b c)) (app_tp l c) (app_tp k c)))
                            (forall_E a c)
                            ))
                            ))
@@ -465,7 +445,7 @@ theory DHOL : ur:?LF =
                                                    
  quotiented_codomain_ax: {A,B,r} (Π A ([x] (B x)∕r)) < (Π A [x] B x)∕([f,g] ∀ A [x] (r (f@x) (g@x))) ❙
   
-  quotiented_codomain: {A,B,r} ({x} x%A ⟶ isEqRel (B x) r) ⟶ isEqRel (Π A [x] B x) ([f,g] ∀ A [x] (r (f@x) (g@x))) ⟶ (Π A [x] B x)∕([f,g] ∀ A [x] (r (f@x) (g@x))) < (Π A ([x] (B x)∕r)) ❘
+  quotiented_codomain_l: {A,B,r} ({x} x%A ⟶ isEqRel (B x) r) ⟶ isEqRel (Π A [x] B x) ([f,g] ∀ A [x] (r (f@x) (g@x))) ⟶ (Π A [x] B x)∕([f,g] ∀ A [x] (r (f@x) (g@x))) < (Π A ([x] (B x)∕r)) ❘
                       = [A,B,r,P,Q] [f,k:f%(Π A [x] B x)∕([u,v] ∀ A [x] (r (u@x) (v@x)))]
                       (quotient_E k 
                       ([g,l:g%(Π A [x] B x),m:⊦g=((Π A [x] B x)∕([u,v] ∀ A [x] (r (u@x) (v@x))))f]
@@ -485,6 +465,9 @@ theory DHOL : ur:?LF =
                       ))
                       )
                       ❙
+                       
+  quotiented_codomain: {A,B,r} ({x} x%A ⟶ isEqRel (B x) r) ⟶ isEqRel (Π A [x] B x) ([f,g] ∀ A [x] (r (f@x) (g@x))) ⟶ (Π A ([x] (B x)∕r)) ≡ (Π A [x] B x)∕([f,g] ∀ A [x] (r (f@x) (g@x))) ❘
+                     = [A,B,r,P,Q] subtp_antisym (quotiented_codomain_ax) (quotiented_codomain_l P Q)❙
                         
  refined_domain: {A,B,p} isEqRel (Π A [x] B x) ([f,g] ∀ A [x] (p x ⇒ (f@x) =(B x) (g@x))) ⟶ (Π A [x] B x)∕([f,g] ∀ A [x] (p x ⇒ (f@x) =(B x) (g@x))) < (Π (A|p) [x] B x) ❘
                = [A,B,p,P] [f,k:f%((Π A [x] B x)∕([g,h] ∀ A [x] (p x ⇒ (g@x) =(B x) (h@x))))]