Definition: p_subset
A ⊆{T} B ==  ∀x:T. ((A x) 
⇒ (B x))
Lemma: p_subset_wf
∀[T:Type]. ∀[A,B:T ⟶ ℙ].  (A ⊆{T} B ∈ ℙ)
Definition: p_equiv
A ≡{T} B ==  A ⊆{T} B ∧ B ⊆{T} A
Lemma: p_equiv_wf
∀[T:Type]. ∀[A,B:T ⟶ ℙ].  (A ≡{T} B ∈ ℙ)
Definition: detach
T-Detach(A) ==  ∀x:T. Dec(A x)
Lemma: detach_wf
∀[T:Type]. ∀[A:T ⟶ ℙ].  (T-Detach(A) ∈ ℙ)
Definition: detach_fun
detach_fun(T;A) ==  {d:T ⟶ 𝔹| ∀x:T. (A x 
⇐⇒ ↑(d x))} 
Lemma: detach_fun_wf
∀[T:Type]. ∀[A:T ⟶ ℙ].  (detach_fun(T;A) ∈ Type)
Lemma: detach_fun_properties
∀[T:Type]. ∀[A:T ⟶ ℙ].  ((∀x:T. SqStable(A x)) 
⇒ (∀d:detach_fun(T;A). {∀x:T. (A x 
⇐⇒ ↑(d x))}))
Lemma: exists_det_fun
∀[T:Type]. ∀[A:T ⟶ ℙ].  ((∀x:T. SqStable(A x)) 
⇒ (detach_fun(T;A) 
⇐⇒ ∀x:T. Dec(A x)))
Lemma: exists_det_fun_a
∀[T:Type]. ∀[A:T ⟶ ℙ].  ((∀x:T. SqStable(A x)) 
⇒ (detach_fun(T;A) 
⇐⇒ {∀x:T. Dec(A x)}))
Lemma: dec_alt_char
∀[T:Type]. ∀[A:T ⟶ ℙ].  (∀x:T. Dec(A x) 
⇐⇒ (∀x:T. SqStable(A x)) ∧ detach_fun(T;A))
Lemma: dec_alt_char_a
∀[T:Type]. ∀[A:T ⟶ ℙ].  (∀x:T. Dec(A x) 
⇐⇒ (∀x:T. SqStable(A x)) ∧ detach_fun(T;A))
Definition: ab_binrel
x,y:T. E[x; y] ==  λx,y. E[x; y]
Lemma: ab_binrel_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (x,y:T. E[x;y] ∈ T ⟶ T ⟶ ℙ)
Lemma: ab_binrel_functionality
∀[T:Type]. ∀[E,E':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (E[x;y] 
⇐⇒ E'[x;y])) 
⇒ ((x,y:T. E[x;y]) <≡>{T} (x,y:T. E'[x;y])))
Definition: binrel_ap
a [r] b ==  r a b
Lemma: binrel_ap_wf
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ]. ∀[a,b:T].  (a [r] b ∈ ℙ)
Lemma: binrel_ap_functionality_wrt_breqv
∀[T:Type]. ∀[r,r':T ⟶ T ⟶ ℙ].  ∀a,b:T.  ((r <≡>{T} r') 
⇒ (a [r] b 
⇐⇒ a [r'] b))
Definition: dec_binrel
dec_binrel(T;r) ==  ∀x,y:T.  Dec(r x y)
Lemma: dec_binrel_wf
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;r) ∈ ℙ)
Definition: xxrefl
(!cond_cons(xxbasic; basic)):: refl(T;E) ==  Refl(T;x,y.E x y)
Lemma: xxrefl_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (refl(T;E) ∈ ℙ)
Lemma: xxrefl_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') 
⇒ (refl(T;R) 
⇐⇒ refl(T;R')))
Definition: xxsym
sym(T;E) ==  Sym(T;x,y.E x y)
Lemma: xxsym_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (sym(T;E) ∈ ℙ)
Lemma: xxsym_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') 
⇒ (sym(T;R) 
⇐⇒ sym(T;R')))
Definition: xxtrans
(!cond_cons(xxbasic; basic)):: trans(T;E) ==  Trans(T;x,y.E x y)
Lemma: xxtrans_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (trans(T;E) ∈ ℙ)
Lemma: xxtrans_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') 
⇒ (trans(T;R) 
⇐⇒ trans(T;R')))
Definition: xxsymmetrize
xxsymmetrize(E) ==  λx,y. ((E x y) ∧ (E y x))
Lemma: xxsymmetrize_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (xxsymmetrize(E) ∈ T ⟶ T ⟶ ℙ)
Definition: xxirrefl
(basic):: irrefl(T;R) ==  Irrefl(T;x,y.R x y)
Lemma: xxirrefl_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (irrefl(T;R) ∈ ℙ)
Definition: xxanti_sym
(!cond_cons(xxbasic; basic)):: anti_sym(T;R) ==  AntiSym(T;x,y.R x y)
Lemma: xxanti_sym_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (anti_sym(T;R) ∈ ℙ)
Lemma: xxanti_sym_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  uiff(anti_sym(T;R);anti_sym(T;R')) supposing R <≡>{T} R'
Definition: xxst_anti_sym
(basic):: st_anti_sym(T;R) ==  StAntiSym(T;x,y.R x y)
Lemma: xxst_anti_sym_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (st_anti_sym(T;R) ∈ ℙ)
Definition: xxconnex
(basic):: connex(T;R) ==  Connex(T;x,y.R x y)
Lemma: xxconnex_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (connex(T;R) ∈ ℙ)
Lemma: xxconnex_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') 
⇒ (connex(T;R) 
⇐⇒ connex(T;R')))
Definition: xxorder
(compound):: order(T;R) ==  refl(T;R) ∧ trans(T;R) ∧ anti_sym(T;R)
Lemma: xxorder_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (order(T;R) ∈ ℙ)
Definition: xxequiv_rel
(compound):: EquivRel(T;R) ==  refl(T;R) ∧ trans(T;R) ∧ sym(T;R)
Lemma: xxequiv_rel_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (EquivRel(T;R) ∈ ℙ)
Lemma: xxorder_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') 
⇒ (order(T;R) 
⇐⇒ order(T;R')))
Lemma: xxorder_eq_order
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (order(T;R) = Order(T;x,y.R x y) ∈ ℙ)
Definition: xxlinorder
xxlinorder(T;R) ==  Linorder(T;x,y.R x y)
Lemma: xxlinorder_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (xxlinorder(T;R) ∈ ℙ)
Definition: refl_cl
Eo ==  λx,y. ((x = y ∈ T) ∨ (E x y))
Lemma: refl_cl_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (Eo ∈ T ⟶ T ⟶ ℙ)
Definition: sym_cl
E↔ ==  λx,y. ((E x y) ∧ (E y x))
Lemma: sym_cl_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (E↔ ∈ T ⟶ T ⟶ ℙ)
Definition: s_part
E\ ==  λx,y. ((E x y) ∧ (¬(E y x)))
Lemma: s_part_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (E\ ∈ T ⟶ T ⟶ ℙ)
Lemma: s_part_functionality_wrt_breqv
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') 
⇒ ((R\) <≡>{T} (R'\)))
Lemma: s_part_char
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[a,b:T].  (((R\) a b) = ((R a b) ∧ (¬(R b a))) ∈ ℙ)
Lemma: xxorder_split
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (order(T;R) 
⇒ (∀x,y:T.  Dec(x = y ∈ T)) 
⇒ (∀a,b:T.  (R a b 
⇐⇒ ((R\) a b) ∨ (a = b ∈ T))))
Lemma: xxtrans_imp_sp_trans
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (trans(T;R) 
⇒ trans(T;R\))
Lemma: refl_cl_is_order
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  trans(T;R) 
⇒ order(T;Ro) supposing irrefl(T;R)
Lemma: irrefl_trans_imp_sasym
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (st_anti_sym(T;R)) supposing (trans(T;R) and irrefl(T;R))
Lemma: xxconnex_iff_trichot
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀a,b:T.  Dec(R a b)) 
⇒ (connex(T;R) 
⇐⇒ {∀a,b:T.  (((R\) a b) ∨ ((R↔) a b) ∨ ((R\) b a))}))
Lemma: xxconnex_iff_trichot_a
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (connex(T;Ro) 
⇐⇒ ∀a,b:T.  ((R a b) ∨ (a = b ∈ T) ∨ (R b a)))
Lemma: rel_le_refl_cl_sp
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;x,y:T. x = y ∈ T) 
⇒ r ≡>{T} (r\\00B8) supposing anti_sym(T;r))
Lemma: refl_cl_sp_le_rel
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (refl(T;r) 
⇒ ((r\\00B8) ≡>{T} r))
Lemma: refl_cl_sp_cancel
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;x,y:T. x = y ∈ T) 
⇒ refl(T;r) 
⇒ (r\\00B8) <≡>{T} r supposing anti_sym(T;r))
Lemma: rel_le_sp_refl_cl
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (r ≡>{T} (ro\)) supposing (st_anti_sym(T;r) and irrefl(T;r))
Lemma: sp_refl_cl_le_rel
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  ((ro\) ≡>{T} r)
Lemma: sp_refl_cl_cancel
∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  ((ro\) <≡>{T} r) supposing (st_anti_sym(T;r) and irrefl(T;r))
Definition: ident
(basic):: Ident(T;op;id) ==  ∀[x:T]. (((x op id) = x ∈ T) ∧ ((id op x) = x ∈ T))
Lemma: ident_wf
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T].  (Ident(T;op;id) ∈ ℙ)
Lemma: sq_stable__ident
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T].  SqStable(Ident(T;op;id))
Definition: bilinear
(basic):: 
BiLinear(T;pl;tm) ==
  ∀[a,x,y:T].  (((a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T) ∧ (((x pl y) tm a) = ((x tm a) pl (y tm a)) ∈ T))
Lemma: bilinear_wf
∀[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].  (BiLinear(T;pl;tm) ∈ ℙ)
Lemma: sq_stable__bilinear
∀[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].  SqStable(BiLinear(T;pl;tm))
Lemma: bilinear_comm_elim
∀[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].
  (BiLinear(T;pl;tm)) supposing ((∀a,x,y:T.  ((a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T)) and Comm(T;tm))
Definition: bilinear_p
(basic):: 
IsBilinear(A;B;C;+a;+b;+c;f) ==
  (∀[a1,a2:A]. ∀[b:B].  (((a1 +a a2) f b) = ((a1 f b) +c (a2 f b)) ∈ C))
  ∧ (∀[a:A]. ∀[b1,b2:B].  ((a f (b1 +b b2)) = ((a f b1) +c (a f b2)) ∈ C))
Lemma: bilinear_p_wf
∀[A,B,C:Type]. ∀[+a:A ⟶ A ⟶ A]. ∀[+b:B ⟶ B ⟶ B]. ∀[+c:C ⟶ C ⟶ C]. ∀[f:A ⟶ B ⟶ C].
  (IsBilinear(A;B;C;+a;+b;+c;f) ∈ ℙ)
Lemma: sq_stable__bilinear_p
∀[A,B,C:Type]. ∀[+a:A ⟶ A ⟶ A]. ∀[+b:B ⟶ B ⟶ B]. ∀[+c:C ⟶ C ⟶ C]. ∀[f:A ⟶ B ⟶ C].
  SqStable(IsBilinear(A;B;C;+a;+b;+c;f))
Definition: action_p
(basic):: IsAction(A;x;e;S;f) ==  (∀[a,b:A].  ∀u:S. (((a x b) f u) = (a f (b f u)) ∈ S)) ∧ (∀[u:S]. ((e f u) = u ∈ S))
Lemma: action_p_wf
∀[A:Type]. ∀[x:A ⟶ A ⟶ A]. ∀[e:A]. ∀[S:Type]. ∀[f:A ⟶ S ⟶ S].  (IsAction(A;x;e;S;f) ∈ ℙ)
Lemma: sq_stable__action_p
∀[A:Type]. ∀[x:A ⟶ A ⟶ A]. ∀[e:A]. ∀[S:Type]. ∀[f:A ⟶ S ⟶ S].  SqStable(IsAction(A;x;e;S;f))
Definition: dist_1op_2op_lr
(basic):: 
Dist1op2opLR(A;1op;2op) ==
  ∀[u,v:A].  (((1op (u 2op v)) = ((1op u) 2op v) ∈ A) ∧ ((1op (u 2op v)) = (u 2op (1op v)) ∈ A))
Lemma: dist_1op_2op_lr_wf
∀[A:Type]. ∀[f:A ⟶ A]. ∀[x:A ⟶ A ⟶ A].  (Dist1op2opLR(A;f;x) ∈ ℙ)
Lemma: sq_stable__dist_1op_2op_lr
∀[A:Type]. ∀[f:A ⟶ A]. ∀[x:A ⟶ A ⟶ A].  SqStable(Dist1op2opLR(A;f;x))
Definition: fun_thru_1op
(basic):: fun_thru_1op(A;B;opa;opb;f) ==  ∀[a:A]. ((f (opa a)) = (opb (f a)) ∈ B)
Lemma: fun_thru_1op_wf
∀[A,B:Type]. ∀[opa:A ⟶ A]. ∀[opb:B ⟶ B]. ∀[f:A ⟶ B].  (fun_thru_1op(A;B;opa;opb;f) ∈ ℙ)
Lemma: sq_stable__fun_thru_1op
∀[A,B:Type]. ∀[opa:A ⟶ A]. ∀[opb:B ⟶ B]. ∀[f:A ⟶ B].  SqStable(fun_thru_1op(A;B;opa;opb;f))
Definition: fun_thru_2op
(basic):: FunThru2op(A;B;opa;opb;f) ==  ∀[a1,a2:A].  ((f (a1 opa a2)) = ((f a1) opb (f a2)) ∈ B)
Lemma: fun_thru_2op_wf
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].  (FunThru2op(A;B;opa;opb;f) ∈ ℙ)
Lemma: sq_stable__fun_thru_2op
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].  SqStable(FunThru2op(A;B;opa;opb;f))
Definition: cancel
(basic):: Cancel(T;S;op) ==  ∀[u,v:T]. ∀[w:S].  u = v ∈ T supposing (w op u) = (w op v) ∈ T
Lemma: cancel_wf
∀[T,S:Type]. ∀[op:S ⟶ T ⟶ T].  (Cancel(T;S;op) ∈ ℙ)
Lemma: sq_stable__cancel
∀[T,S:Type]. ∀[op:S ⟶ T ⟶ T].  SqStable(Cancel(T;S;op))
Definition: monot
(basic):: monot(T;x,y.R[x; y];f) ==  ∀x,y:T.  (R[x; y] 
⇒ R[f x; f y])
Lemma: monot_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[f:T ⟶ T].  (monot(T;x,y.R[x;y];f) ∈ ℙ)
Lemma: sq_stable__monot
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀f:T ⟶ T. ((∀x,y:T.  SqStable(R[x;y])) 
⇒ SqStable(monot(T;x,y.R[x;y];f)))
Lemma: monot_functionality
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ∀f:T ⟶ T. ((∀x,y:T.  (R[x;y] 
⇐⇒ R'[x;y])) 
⇒ (monot(T;x,y.R[x;y];f) 
⇐⇒ monot(T;x,y.R'[x;y];f)))
Definition: monotone
monotone(T;T';x,y.R[x; y];x,y.R'[x; y];f) ==  ∀x,y:T.  (R[x; y] 
⇒ R'[f x; f y])
Lemma: monotone_wf
∀[T,T':Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[R':T' ⟶ T' ⟶ ℙ]. ∀[f:T ⟶ T'].  (monotone(T;T';x,y.R[x;y];x,y.R'[x;y];f) ∈ ℙ)
Definition: rels_iso
(basic):: RelsIso(T;T';x,y.R[x; y];x,y.R'[x; y];f) ==  ∀x,y:T.  (R[x; y] 
⇐⇒ R'[f x; f y])
Lemma: rels_iso_wf
∀[T,T':Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[R':T' ⟶ T' ⟶ ℙ]. ∀[f:T ⟶ T'].  (RelsIso(T;T';x,y.R[x;y];x,y.R'[x;y];f) ∈ ℙ)
Lemma: assoc_shift
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].
  (Assoc(A;opa)) supposing (Assoc(B;opb) and FunThru2op(A;B;opa;opb;f) and Inj(A;B;f))
Lemma: comm_shift
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].
  (Comm(A;opa)) supposing (Comm(B;opb) and FunThru2op(A;B;opa;opb;f) and Inj(A;B;f))
Lemma: cancel_shift
∀[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].
  (Cancel(A;A;opa)) supposing (Cancel(B;B;opb) and FunThru2op(A;B;opa;opb;f) and Inj(A;B;f))
Lemma: eqfun_p_shift
∀[A,B:Type]. ∀[eqa:A ⟶ A ⟶ 𝔹]. ∀[eqb:B ⟶ B ⟶ 𝔹]. ∀[f:A ⟶ B].
  (IsEqFun(A;eqa)) supposing (IsEqFun(B;eqb) and RelsIso(A;B;x,y.↑(x eqa y);x,y.↑(x eqb y);f) and Inj(A;B;f))
Lemma: sym_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B. (RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) 
⇒ Sym(B;x,y.S[x;y]) 
⇒ Sym(A;x,y.R[x;y]))
Lemma: usym_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B
    ((∀[x,y:A].  R[x;y] supposing R[x;y])
    
⇒ RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)
    
⇒ UniformlySym(B;x,y.S[x;y])
    
⇒ UniformlySym(A;x,y.R[x;y]))
Lemma: trans_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B. (RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) 
⇒ Trans(B;x,y.S[x;y]) 
⇒ Trans(A;x,y.R[x;y]))
Lemma: utrans_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B
    ((∀[x,y:A].  R[x;y] supposing R[x;y])
    
⇒ RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)
    
⇒ UniformlyTrans(B;x,y.S[x;y])
    
⇒ UniformlyTrans(A;x,y.R[x;y]))
Lemma: connex_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B. (RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) 
⇒ Connex(B;x,y.S[x;y]) 
⇒ Connex(A;x,y.R[x;y]))
Lemma: anti_sym_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ]. ∀[f:A ⟶ B].
  (AntiSym(A;x,y.R[x;y])) supposing (AntiSym(B;x,y.S[x;y]) and RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) and Inj(A;B;f))
Lemma: uanti_sym_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ]. ∀[f:A ⟶ B].
  (UniformlyAntiSym(A;x,y.R[x;y])) supposing 
     (UniformlyAntiSym(B;x,y.S[x;y]) and 
     RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) and 
     Inj(A;B;f))
Lemma: refl_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B. (RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) 
⇒ Refl(B;x,y.S[x;y]) 
⇒ Refl(A;x,y.R[x;y]))
Lemma: urefl_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B
    ((∀[x,y:A].  R[x;y] supposing R[x;y])
    
⇒ RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f)
    
⇒ UniformlyRefl(B;x,y.S[x;y])
    
⇒ UniformlyRefl(A;x,y.R[x;y]))
Lemma: monot_shift
∀[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[S:B ⟶ B ⟶ ℙ].
  ∀opa:A ⟶ A. ∀opb:B ⟶ B. ∀f:A ⟶ B.
    RelsIso(A;B;x,y.R[x;y];x,y.S[x;y];f) 
⇒ monot(B;x,y.S[x;y];opb) 
⇒ monot(A;x,y.R[x;y];opa) 
    supposing fun_thru_1op(A;B;opa;opb;f)
Home
Index