Definition: p_subset
A ⊆{T} ==  ∀x:T. ((A x)  (B x))

Lemma: p_subset_wf
[T:Type]. ∀[A,B:T ⟶ ℙ].  (A ⊆{T} B ∈ ℙ)

Definition: p_equiv
A ≡{T} ==  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 ⇐⇒ ↑(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 ⇐⇒ ↑(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
[r] ==  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] ⇐⇒ [r'] b))

Definition: dec_binrel
dec_binrel(T;r) ==  ∀x,y:T.  Dec(r 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 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 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 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 y) ∧ (E x))

Lemma: xxsymmetrize_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (xxsymmetrize(E) ∈ T ⟶ T ⟶ ℙ)

Definition: xxirrefl
(basic):: irrefl(T;R) ==  Irrefl(T;x,y.R 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 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 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 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 y) ∈ ℙ)

Definition: xxlinorder
xxlinorder(T;R) ==  Linorder(T;x,y.R y)

Lemma: xxlinorder_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (xxlinorder(T;R) ∈ ℙ)

Definition: refl_cl
Eo ==  λx,y. ((x y ∈ T) ∨ (E y))

Lemma: refl_cl_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (Eo ∈ T ⟶ T ⟶ ℙ)

Definition: sym_cl
E ==  λx,y. ((E y) ∧ (E x))

Lemma: sym_cl_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (E ∈ T ⟶ T ⟶ ℙ)

Definition: s_part
E\ ==  λx,y. ((E y) ∧ (E 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\) b) ((R b) ∧ (R a))) ∈ ℙ)

Lemma: xxorder_split
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (order(T;R)  (∀x,y:T.  Dec(x y ∈ T))  (∀a,b:T.  (R ⇐⇒ ((R\) 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;Rosupposing 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 b))  (connex(T;R) ⇐⇒ {∀a,b:T.  (((R\) b) ∨ ((Rb) ∨ ((R\) a))}))

Lemma: xxconnex_iff_trichot_a
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (connex(T;Ro⇐⇒ ∀a,b:T.  ((R b) ∨ (a b ∈ T) ∨ (R a)))

Lemma: rel_le_refl_cl_sp
[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;x,y:T. 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. y ∈ T)  refl(T;r)  (r\\00B8) <≡>{T} 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) b) ((a1 b) +c (a2 b)) ∈ C))
  ∧ (∀[a:A]. ∀[b1,b2:B].  ((a (b1 +b b2)) ((a b1) +c (a 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 b) u) (a (b u)) ∈ S)) ∧ (∀[u:S]. ((e 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].  v ∈ 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; 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; 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; 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