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 (valid_eq_flip (and_I T (eq_refl (refine_I P T))) (app_sub_eq_simple P Q R ([x,k:x%A] and_tp (S x k) ([l:⊦p x] eq_tp (refine_I k l) (refine_I P 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_simple A B ([x] x) x y P Q S ([u,v:u%A] R u v)❙
= [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 ❘
= [F,G,P,Q,R,S] eq_trans (props_in_true2 F P R) (props_in_true2 true true_tp trueI) (props_in_true2 G Q S) (true_props_at_true (props_in_true2 F P R)) (eq_sym (true_props_at_true (props_in_true2 G Q S)))❙
both_true_equalsv: {F,G} F%(bool|[x] x =bool true) ⟶ G%(bool|[x] x =bool true) ⟶ ⊦F =(bool|[x] x =bool true) G ❘
= [A,r,rˈ,P,Q,R] subtp_antisym ([s,l:s%(A∕r)∕rˈ] quo_E l
([y,n:y%(A∕r),o] (rep_quo_help P Q R) y n)
([y,z, n:y%(A∕r),o:z%(A∕r), p,q] valid_eq_flip
(quo_eq_E n o
(quo_min_impl (rep_quo_help P Q R) Q
(EqRel_isBinRel quo_triv)
([u:tm,v:tm, f:u%A∕r,g:v%A∕r, h:⊦rˈ@u@v] valid_eq
(impl_E (props_in_true (quo_eq_Iv ((rep_quo_help P Q R) u f) ((rep_quo_help P Q R) v g) (p_BinRel ([a,b, k:a%A,m:b%A] BinRel_tp Q (quo_I k quo_form P) (quo_I m quo_form P)))))
h)
(lemma_double_lam ((rep_quo_help P Q R) u f) ((rep_quo_help P Q R) v g))
)
(EqRel_isExt quo_triv))
eq_trans (quo_I n quo_form Q) l (quo_I o quo_form Q) p (eq_sym q))
(lemma_double_lam ((rep_quo_help P Q R) y n) ((rep_quo_help P Q R) z o))
))
(quo_sub (quo_subtp P) (p_BinRel ([x,y, k:x%A,l:y%A] BinRel_tp Q (quo_I k quo_form P) (quo_I l quo_form P))) Q ([x,y, kˈ,lˈ, m] m ))
❙
quo_in_ref_subtp: {A,r,p} r%BinRel A ⟶ ({x} x%A ⟶ p x%bool) ⟶ r%BinRel (A|p) ❘
(eq_trans (quo_I l quo_form (quo_in_ref_subtp P ([u,v] Q u (quo_I v quo_form P)))) k (quo_I m quo_form (quo_in_ref_subtp P ([u,v] Q u (quo_I v quo_form P)))) n (eq_sym o))
)
(lemma_double_lam_quo_ref P Q l m)
)
❙
rep_ref_quo: {A,r,p} r%BinRel A ⟶ ({x} x%A∕r ⟶ p x%bool) ⟶ (A∕r)|p < (A|p)∕r ❘
quoed_domain: {A,B,r} r%BinRel A ⟶ (Π (A∕r) [x] B x) ≡ (Π A [x] B x)|([f] ∀ A [x] (∀ A [y] (r@x@y ⇒ (f@x) =(B x) (f@y)))) ❘
= [A,B,r,P] subtp_antisym ([f,k:f%(Π (A∕r) [x] B x)]
refine_I
(exten_tp ([y,l:y%A] app_tp k quo_I l quo_form P))
(forall_I ([x,l:x%A]
forall_I ([y,m:y%A]
impl_I [n] (app_eq (eq_refl k) (quo_eq_I l m P n))))))
([f,k:f%(Π A [x] B x)|([g] ∀ A [x] (∀ A [y] (r@x@y ⇒ (g@x) =(B x) (g@y))))] exten_tp
([s,l:s%A∕r] quo_Ev l
([x,m:x%A,n:⊦x=(A∕r)s] app_tp (refine_E1 k) m)
([x,y, m:x%A,n:y%A, o:⊦x=(A∕r)s,p:⊦y=(A∕r)s, q]
impl_E
(forall_E (forall_E (refine_E2 k) m) n)
q)))
❙
quoed_codomain_ax: {A,B,r} (Π A ([x] (B x)∕r)) < (Π A [x] B x)∕(λ (Π A [x] B x) ([f] λ (Π A [x] B x) ([g] ∀ A [x] r@(f@x)@(g@x)))) ❙
quoed_codomain_l: {A,B,r} ({x} x%A ⟶ r%BinRel (B x)) ⟶ (Π A [x] B x)∕(λ (Π A [x] B x) ([f] λ (Π A [x] B x) ([g] ∀ A [x] r@(f@x)@(g@x)))) < (Π A ([x] (B x)∕r)) ❘
= [A,B,r,P] [f,k]
quo_Ev k
([g,l,m]
exten_tp ([x,n:x%A] quo_I (app_tp l n) (quo_form P x n))
)
([g,h, l,m, n,o, q]
exten_eq ([z,p:z%A]
quo_eq_I (app_tp l p) (app_tp m p) (P z p) (forall_E
(valid_eq_flip q
(eq_trans
(app_tp (app_tp (lam_tp eqtp_refl ([a,b] lam_tp eqtp_refl ([c,d] forall_tp ([u,v] BinRel_tp (P u v) (app_tp b v) (app_tp d v))))) l) m)
(app_tp (lam_tp eqtp_refl ([c,d] forall_tp ([u,v] BinRel_tp (P u v) (app_tp l v) (app_tp d v)))) m)
(forall_tp ([u,v] BinRel_tp (P u v) (app_tp l v) (app_tp m v)))
(app_eq (lam_beta ([uˈ,vˈ] app_tp (lam_tp eqtp_refl ([a,b] lam_tp eqtp_refl ([c,d] forall_tp ([u,v] BinRel_tp (P u v) (app_tp b v) (app_tp d v))))) vˈ) l) (eq_refl m))
(lam_beta ([uˈ,vˈ] app_tp (lam_tp eqtp_refl ([c,d] forall_tp ([u,v] BinRel_tp (P u v) (app_tp l v) (app_tp d v)))) vˈ) m)))
p)))
❙
quoed_codomain: {A,B,r} ({x} x%A ⟶ r%BinRel (B x)) ⟶ (Π A ([x] (B x)∕r)) ≡ (Π A [x] B x)∕(λ (Π A [x] B x) ([f] λ (Π A [x] B x) ([g] ∀ A [x] r@(f@x)@(g@x)))) ❘
refined_domain: {A,B,p} ({x} x%A ⟶ p x%bool) ⟶ (λ (Π A [x] B x) ([f] λ (Π A [x] B x) ([g] ∀ A [x] (p x ⇒ (f@x) =(B x) (g@x)))))%BinRel (Π A [x] B x) ⟶ (Π A [x] B x)∕(λ (Π A [x] B x) ([f] λ (Π A [x] B x) ([g] ∀ A [x] (p x ⇒ (f@x) =(B x) (g@x))))) < (Π (A|p) [x] B x) ❘
= [A,B,p,P,Q] [f,k]
quo_Ev k ([g,m, u] exten_tp ([x,l] app_tp m (refine_E1 l)))
([g,h, m,n, o,q, w]
exten_eq ([x,l:x%A|p]
impl_E
(forall_E
(valid_eq_flip w
(eq_trans
(app_tp (app_tp (lam_tp eqtp_refl ([a,b] lam_tp eqtp_refl ([c,d] forall_tp ([u,v] impl_tp_nondep (P u v) (eq_tp (app_tp b v) (app_tp d v)))))) m) n)
(app_tp (lam_tp eqtp_refl ([c,d] forall_tp ([u,v] impl_tp_nondep (P u v) (eq_tp (app_tp m v) (app_tp d v))))) n)
(forall_tp ([u,v] impl_tp_nondep (P u v) (eq_tp (app_tp m v) (app_tp n v))))
(app_eq (lam_beta ([uˈ,vˈ] app_tp (lam_tp eqtp_refl ([a,b] lam_tp eqtp_refl ([c,d] forall_tp ([u,v] impl_tp_nondep (P u v) (eq_tp (app_tp b v) (app_tp d v)))))) vˈ) m) (eq_refl n))
(lam_beta ([uˈ,vˈ] app_tp (lam_tp eqtp_refl ([c,d] forall_tp ([u,v] impl_tp_nondep (P u v) (eq_tp (app_tp m v) (app_tp d v))))) vˈ) n)))
