Library Ssreflect.ssrbool

Require Import ssreflect.
Require Import ssrfun.
Require Export Bool.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Reserved Notation "~~ b" (at level 35, right associativity).
Reserved Notation "b ==> c" (at level 55, right associativity).
Reserved Notation "b1 (+) b2" (at level 50, left associativity).
Reserved Notation "x \in A" (at level 70, no associativity).
Reserved Notation "x \notin A" (at level 70, no associativity).
Reserved Notation "p1 =i p2" (at level 70, no associativity).


Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing).
Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format
  "'[hv' [ /\ '[' P1 , '/' P2 ']' '/ ' & P3 ] ']'").
Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format
  "'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 ']' '/ ' & P4 ] ']'").
Reserved Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" (at level 0, format
  "'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 , '/' P4 ']' '/ ' & P5 ] ']'").

Reserved Notation "[ \/ P1 | P2 ]" (at level 0, only parsing).
Reserved Notation "[ \/ P1 , P2 | P3 ]" (at level 0, format
  "'[hv' [ \/ '[' P1 , '/' P2 ']' '/ ' | P3 ] ']'").
Reserved Notation "[ \/ P1 , P2 , P3 | P4 ]" (at level 0, format
  "'[hv' [ \/ '[' P1 , '/' P2 , '/' P3 ']' '/ ' | P4 ] ']'").

Reserved Notation "[ && b1 & c ]" (at level 0, only parsing).
Reserved Notation "[ && b1 , b2 , .. , bn & c ]" (at level 0, format
  "'[hv' [ && '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' & c ] ']'").

Reserved Notation "[ || b1 | c ]" (at level 0, only parsing).
Reserved Notation "[ || b1 , b2 , .. , bn | c ]" (at level 0, format
  "'[hv' [ || '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' | c ] ']'").

Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing).
Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format
  "'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'").

Reserved Notation "[ 'pred' : T => E ]" (at level 0, format

  "'[hv' [ 'pred' : T => '/ ' E ] ']'").
Reserved Notation "[ 'pred' x => E ]" (at level 0, x at level 8, format
  "'[hv' [ 'pred' x => '/ ' E ] ']'").
Reserved Notation "[ 'pred' x : T => E ]" (at level 0, x at level 8, format
  "'[hv' [ 'pred' x : T => '/ ' E ] ']'").

Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format
  "'[hv' [ 'rel' x y => '/ ' E ] ']'").
Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format
  "'[hv' [ 'rel' x y : T => '/ ' E ] ']'").


Delimit Scope bool_scope with B.


Arguments Scope negb [bool_scope].
Arguments Scope orb [bool_scope bool_scope].
Arguments Scope xorb [bool_scope bool_scope].
Arguments Scope andb [bool_scope bool_scope].
Arguments Scope implb [bool_scope bool_scope].
Arguments Scope eqb [bool_scope bool_scope].
Arguments Scope leb [bool_scope bool_scope].
Arguments Scope ifb [bool_scope bool_scope bool_scope].


Definition addb b := if b then negb else fun b' => b'.


Notation "~~ b" := (negb b) : bool_scope.
Notation "b ==> c" := (implb b c) : bool_scope.
Notation "b1 (+) b2" := (addb b1 b2) : bool_scope.


Coercion is_true b := b = true.

Lemma prop_congr : forall b b' : bool, b = b' -> b = b' :> Prop.
Proof. by move=> b b' ->. Qed.

Ltac prop_congr := apply: prop_congr.

Lemma is_true_true : true. Proof. by []. Qed.
Lemma not_false_is_true : ~ false. Proof. by []. Qed.
Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
Hint Resolve is_true_true not_false_is_true is_true_locked_true.

Definition isT := is_true_true.
Definition notF := not_false_is_true.



Lemma negbT : forall b, b = false -> ~~ b. Proof. by case. Qed.
Lemma negbTE : forall b, ~~ b -> b = false. Proof. by case. Qed.
Lemma negbF : forall b : bool, b -> ~~ b = false. Proof. by case. Qed.
Lemma negbFE : forall b, ~~ b = false -> b. Proof. by case. Qed.
Lemma negbK : involutive negb. Proof. by case. Qed.
Lemma negbNE : forall b, ~~ ~~ b -> b. Proof. by case. Qed.

Lemma negb_inj : injective negb. Proof. exact: can_inj negbK. Qed.

Lemma negbLR : forall b c, b = ~~ c -> ~~ b = c.
Proof. by move=> ? [] ->. Qed.

Lemma negbRL : forall b c, ~~ b = c -> b = ~~ c.
Proof. by move=> [] ? <-. Qed.

Lemma contra : forall c b : bool, (c -> b) -> ~~ b -> ~~ c.
Proof. by do 2!case. Qed.
Definition contraNN := contra.

Lemma contraL : forall c b : bool, (c -> ~~ b) -> b -> ~~ c.
Proof. by do 2!case. Qed.
Definition contraTN := contraL.

Lemma contraR : forall c b : bool, (~~ c -> b) -> ~~ b -> c.
Proof. by do 2!case. Qed.
Definition contraNT := contraR.

Lemma contraLR : forall c b : bool, (~~ c -> ~~ b) -> b -> c.
Proof. by do 2!case. Qed.
Definition contraTT := contraLR.

Lemma contraT : forall b, (~~ b -> false) -> b. Proof. by case=> // ->. Qed.

Lemma wlog_neg : forall b, (~~ b -> b) -> b. Proof. by case=> // ->. Qed.

Lemma contraFT : forall c b : bool, (~~ c -> b) -> b = false -> c.
Proof. by case=> [] [] // ->. Qed.

Lemma contraFN : forall c b : bool, (c -> b) -> b = false -> ~~ c.
Proof. by case=> [] [] //= ->. Qed.

Lemma contraTF : forall c b : bool, (c -> ~~ b) -> b -> c = false.
Proof. by case=> [] [] //= ->. Qed.

Lemma contraNF : forall c b : bool, (c -> b) -> ~~ b -> c = false.
Proof. by case=> [] [] // ->. Qed.

Lemma contraFF : forall c b : bool, (c -> b) -> b = false -> c = false.
Proof. by case=> [] [] // ->. Qed.


Coercion isSome T (u : option T) := if u is Some _ then true else false.

Coercion is_inl A B (u : A + B) := if u is inl _ then true else false.

Coercion is_left A B (u : {A} + {B}) := if u is left _ then true else false.

Coercion is_inleft A B (u : A + {B}) := if u is inleft _ then true else false.

Prenex Implicits isSome is_inl is_left is_inleft.


Section BoolIf.

Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).

CoInductive if_spec (not_b : Prop) : bool -> A -> Set :=
  | IfSpecTrue of b : if_spec not_b true vT
  | IfSpecFalse of not_b : if_spec not_b false vF.

Lemma ifP : if_spec (b = false) b (if b then vT else vF).
Proof. by case def_b: b; constructor. Qed.

Lemma ifPn : if_spec (~~ b) b (if b then vT else vF).
Proof. by case def_b: b; constructor; rewrite ?def_b. Qed.

Lemma if_same : (if b then vT else vT) = vT.
Proof. by case b. Qed.

Lemma if_neg : (if ~~ b then vT else vF) = if b then vF else vT.
Proof. by case b. Qed.

Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.
Proof. by case b. Qed.

Lemma if_arg : forall fT fF : A -> B,
  (if b then fT else fF) x = if b then fT x else fF x.
Proof. by case b. Qed.


Definition if_expr := if b then vT else vF.
Lemma ifE : (if b then vT else vF) = if_expr. Proof. by []. Qed.

End BoolIf.


Inductive reflect (P : Prop) : bool -> Set :=
  | ReflectT of P : reflect P true
  | ReflectF of ~ P : reflect P false.


Section ReflectCore.

Variables (P Q : Prop) (b c : bool).

Hypothesis Hb : reflect P b.

Lemma introNTF : (if c then ~ P else P) -> ~~ b = c.
Proof. by case c; case Hb. Qed.

Lemma introTF : (if c then P else ~ P) -> b = c.
Proof. by case c; case Hb. Qed.

Lemma elimNTF : ~~ b = c -> if c then ~ P else P.
Proof. by move <-; case Hb. Qed.

Lemma elimTF : b = c -> if c then P else ~ P.
Proof. by move <-; case Hb. Qed.

Lemma equivPif : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q.
Proof. by case Hb; auto. Qed.

Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q.
Proof. by case Hb => [? _ H ? | ? H _]; case: H. Qed.

End ReflectCore.

Section ReflectNegCore.

Variables (P Q : Prop) (b c : bool).
Hypothesis Hb : reflect P (~~ b).

Lemma introTFn : (if c then ~ P else P) -> b = c.
Proof. by move/(introNTF Hb) <-; case b. Qed.

Lemma elimTFn : b = c -> if c then ~ P else P.
Proof. by move <-; apply: (elimNTF Hb); case b. Qed.

Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q.
Proof. rewrite -if_neg; exact: equivPif. Qed.

Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q.
Proof. rewrite -if_neg; exact: xorPif. Qed.

End ReflectNegCore.

Section Reflect.

Variables (P Q : Prop) (b b' c : bool).
Hypotheses (Pb : reflect P b) (Pb' : reflect P (~~ b')).

Lemma introT : P -> b. Proof. exact: introTF true _. Qed.
Lemma introF : ~ P -> b = false. Proof. exact: introTF false _. Qed.
Lemma introN : ~ P -> ~~ b. Proof. exact: introNTF true _. Qed.
Lemma introNf : P -> ~~ b = false. Proof. exact: introNTF false _. Qed.
Lemma introTn : ~ P -> b'. Proof. exact: introTFn true _. Qed.
Lemma introFn : P -> b' = false. Proof. exact: introTFn false _. Qed.

Lemma elimT : b -> P. Proof. exact: elimTF true _. Qed.
Lemma elimF : b = false -> ~ P. Proof. exact: elimTF false _. Qed.
Lemma elimN : ~~ b -> ~P. Proof. exact: elimNTF true _. Qed.
Lemma elimNf : ~~ b = false -> P. Proof. exact: elimNTF false _. Qed.
Lemma elimTn : b' -> ~ P. Proof. exact: elimTFn true _. Qed.
Lemma elimFn : b' = false -> P. Proof. exact: elimTFn false _. Qed.

Lemma introP : (b -> Q) -> (~~ b -> ~ Q) -> reflect Q b.
Proof. by case b; constructor; auto. Qed.

Lemma iffP : (P -> Q) -> (Q -> P) -> reflect Q b.
Proof. by case: Pb; constructor; auto. Qed.

Lemma appP : reflect Q b -> P -> Q.
Proof. by move=> Qb; move/introT; case: Qb. Qed.

Lemma sameP : reflect P c -> b = c.
Proof. case; [exact: introT | exact: introF]. Qed.

Lemma decPcases : if b then P else ~ P. Proof. by case Pb. Qed.

Definition decP : {P} + {~ P}. by case: b decPcases; [left | right]. Defined.

Lemma rwP : P <-> b. Proof. by split; [exact: introT | exact: elimT]. Qed.

Lemma rwP2 : reflect Q b -> (P <-> Q).
Proof. by move=> Qb; split=> ?; [exact: appP | apply: elimT; case: Qb]. Qed.


End Reflect.

Hint View for move/ elimTF|3 elimNTF|3 elimTFn|3 introT|2 introTn|2 introN|2.

Hint View for apply/ introTF|3 introNTF|3 introTFn|3 elimT|2 elimTn|2 elimN|2.

Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.

Coercion elimT : reflect >-> Funclass.

Section BooleanAlternative.

Variables (T : Type) (bP : T -> bool) (a : T).

CoInductive alt_spec (P : T -> Prop) : bool -> Type :=
  | AltTrue of P a : alt_spec P true
  | AltFalse of ~~ bP a : alt_spec P false.

Lemma altP : forall P, reflect P (bP a) -> alt_spec (fun _ : T => P) (bP a).
Proof. by move=> P; case bPa: (bP a) /; constructor; rewrite ?bPa. Qed.


Lemma boolP_proof : phantom bool (bP a) -> alt_spec [eta bP] (bP a).
Proof. by move=> _; case bPa: (bP a); constructor; rewrite ?bPa. Qed.

End BooleanAlternative.

Notation boolP b := (boolP_proof (@Phantom bool b%B)).

Definition classically P := forall b : bool, (P -> b) -> b.

Lemma classicP : forall P : Prop, classically P <-> ~ ~ P.
Proof.
move=> P; split=> [cP nP | nnP [] // nP]; last by case nnP; move/nP.
by have: P -> false; [move/nP | move/cP].
Qed.

Lemma classic_bind : forall P Q,
  (P -> classically Q) -> (classically P -> classically Q).
Proof. by move=> P Q IH IH_P b IH_Q; apply: IH_P; move/IH; exact. Qed.

Lemma classic_EM : forall P, classically ({P} + {~ P}).
Proof.
by move=> P [] // IH; apply IH; right => ?; apply: notF (IH _); left.
Qed.

Lemma classic_imply : forall P Q, (P -> classically Q) -> classically (P -> Q).
Proof.
move=> P Q IH [] // notPQ; apply notPQ; move/IH=> hQ; case: notF.
by apply: hQ => hQ; case: notF; exact: notPQ.
Qed.

Lemma classic_pick : forall T P,
  classically ({x : T | P x} + (forall x, ~ P x)).
Proof.
move=> T P [] // IH; apply IH; right=> x Px; case: notF.
by apply: IH; left; exists x.
Qed.


Inductive and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3.

Inductive and4 (P1 P2 P3 P4 : Prop) : Prop := And4 of P1 & P2 & P3 & P4.

Inductive and5 (P1 P2 P3 P4 P5 : Prop) : Prop :=
  And5 of P1 & P2 & P3 & P4 & P5.

Inductive or3 (P1 P2 P3 : Prop) : Prop := Or31 of P1 | Or32 of P2 | Or33 of P3.

Inductive or4 (P1 P2 P3 P4 : Prop) : Prop :=
  Or41 of P1 | Or42 of P2 | Or43 of P3 | Or44 of P4.

Notation "[ /\ P1 & P2 ]" := (and P1 P2) (only parsing) : type_scope.
Notation "[ /\ P1 , P2 & P3 ]" := (and3 P1 P2 P3) : type_scope.
Notation "[ /\ P1 , P2 , P3 & P4 ]" := (and4 P1 P2 P3 P4) : type_scope.
Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" := (and5 P1 P2 P3 P4 P5) : type_scope.

Notation "[ \/ P1 | P2 ]" := (or P1 P2) (only parsing) : type_scope.
Notation "[ \/ P1 , P2 | P3 ]" := (or3 P1 P2 P3) : type_scope.
Notation "[ \/ P1 , P2 , P3 | P4 ]" := (or4 P1 P2 P3 P4) : type_scope.

Notation "[ && b1 & c ]" := (b1 && c) (only parsing) : bool_scope.
Notation "[ && b1 , b2 , .. , bn & c ]" := (b1 && (b2 && .. (bn && c) .. ))
  : bool_scope.

Notation "[ || b1 | c ]" := (b1 || c) (only parsing) : bool_scope.
Notation "[ || b1 , b2 , .. , bn | c ]" := (b1 || (b2 || .. (bn || c) .. ))
  : bool_scope.

Notation "[ ==> b1 , b2 , .. , bn => c ]" :=
   (b1 ==> (b2 ==> .. (bn ==> c) .. )) : bool_scope.
Notation "[ ==> b1 => c ]" := (b1 ==> c) (only parsing) : bool_scope.

Section ReflectConnectives.

Variable b1 b2 b3 b4 b5 : bool.

Lemma idP : reflect b1 b1.
Proof. by case b1; constructor. Qed.

Lemma idPn : reflect (~~ b1) (~~ b1).
Proof. by case b1; constructor. Qed.

Lemma negP : reflect (~ b1) (~~ b1).
Proof. by case b1; constructor; auto. Qed.

Lemma negPn : reflect b1 (~~ ~~ b1).
Proof. by case b1; constructor. Qed.

Lemma negPf : reflect (b1 = false) (~~ b1).
Proof. by case b1; constructor. Qed.

Lemma andP : reflect (b1 /\ b2) (b1 && b2).
Proof. by case b1; case b2; constructor=> //; case. Qed.

Lemma and3P : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3].
Proof. by case b1; case b2; case b3; constructor; try by case. Qed.

Lemma and4P : reflect [/\ b1, b2, b3 & b4] [&& b1, b2, b3 & b4].
Proof.
by case b1; case b2; case b3; case b4; constructor; try by case. Qed.

Lemma and5P : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5].
Proof.
by case b1; case b2; case b3; case b4; case b5; constructor; try by case.
Qed.

Lemma orP : reflect (b1 \/ b2) (b1 || b2).
Proof. by case b1; case b2; constructor; auto; case. Qed.

Lemma or3P : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3].
Proof.
case b1; first by constructor; constructor 1.
case b2; first by constructor; constructor 2.
case b3; first by constructor; constructor 3.
by constructor; case.
Qed.

Lemma or4P : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4].
Proof.
case b1; first by constructor; constructor 1.
case b2; first by constructor; constructor 2.
case b3; first by constructor; constructor 3.
case b4; first by constructor; constructor 4.
by constructor; case.
Qed.

Lemma nandP : reflect (~~ b1 \/ ~~ b2) (~~ (b1 && b2)).
Proof. by case b1; case b2; constructor; auto; case; auto. Qed.

Lemma norP : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)).
Proof. by case b1; case b2; constructor; auto; case; auto. Qed.

Lemma implyP : reflect (b1 -> b2) (b1 ==> b2).
Proof. by case b1; case b2; constructor; auto. Qed.

End ReflectConnectives.

Implicit Arguments idP [b1].
Implicit Arguments idPn [b1].
Implicit Arguments negP [b1].
Implicit Arguments negPn [b1].
Implicit Arguments negPf [b1].
Implicit Arguments andP [b1 b2].
Implicit Arguments and3P [b1 b2 b3].
Implicit Arguments and4P [b1 b2 b3 b4].
Implicit Arguments and5P [b1 b2 b3 b4 b5].
Implicit Arguments orP [b1 b2].
Implicit Arguments or3P [b1 b2 b3].
Implicit Arguments or4P [b1 b2 b3 b4].
Implicit Arguments nandP [b1 b2].
Implicit Arguments norP [b1 b2].
Implicit Arguments implyP [b1 b2].
Prenex Implicits idP idPn negP negPn negPf.
Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.


Lemma andTb : left_id true andb. Proof. by []. Qed.
Lemma andFb : left_zero false andb. Proof. by []. Qed.
Lemma andbT : right_id true andb. Proof. by case. Qed.
Lemma andbF : right_zero false andb. Proof. by case. Qed.
Lemma andbb : idempotent andb. Proof. by case. Qed.
Lemma andbC : commutative andb. Proof. by do 2!case. Qed.
Lemma andbA : associative andb. Proof. by do 3!case. Qed.
Lemma andbCA : left_commutative andb. Proof. by do 3!case. Qed.
Lemma andbAC : right_commutative andb. Proof. by do 3!case. Qed.

Lemma orTb : forall b, true || b. Proof. by []. Qed.
Lemma orFb : left_id false orb. Proof. by []. Qed.
Lemma orbT : forall b, b || true. Proof. by case. Qed.
Lemma orbF : right_id false orb. Proof. by case. Qed.
Lemma orbb : idempotent orb. Proof. by case. Qed.
Lemma orbC : commutative orb. Proof. by do 2!case. Qed.
Lemma orbA : associative orb. Proof. by do 3!case. Qed.
Lemma orbCA : left_commutative orb. Proof. by do 3!case. Qed.
Lemma orbAC : right_commutative orb. Proof. by do 3!case. Qed.

Lemma andbN : forall b, b && ~~ b = false. Proof. by case. Qed.
Lemma andNb : forall b, ~~ b && b = false. Proof. by case. Qed.
Lemma orbN : forall b, b || ~~ b = true. Proof. by case. Qed.
Lemma orNb : forall b, ~~ b || b = true. Proof. by case. Qed.

Lemma andb_orl : left_distributive andb orb. Proof. by do 3!case. Qed.
Lemma andb_orr : right_distributive andb orb. Proof. by do 3!case. Qed.
Lemma orb_andl : left_distributive orb andb. Proof. by do 3!case. Qed.
Lemma orb_andr : right_distributive orb andb. Proof. by do 3!case. Qed.

Lemma andb_idl : forall a b : bool, (b -> a) -> a && b = b.
Proof. by case=> [] [] // ->. Qed.
Lemma andb_idr : forall a b : bool, (a -> b) -> a && b = a.
Proof. by case=> [] [] // ->. Qed.
Lemma andb_id2l : forall a b c : bool, (a -> b = c) -> a && b = a && c.
Proof. by case=> [] [] [] // ->. Qed.
Lemma andb_id2r : forall a b c : bool, (b -> a = c) -> a && b = c && b.
Proof. by case=> [] [] [] // ->. Qed.

Lemma orb_idl : forall a b : bool, (a -> b) -> a || b = b.
Proof. by case=> [] [] // ->. Qed.
Lemma orbb_idr : forall a b : bool, (b -> a) -> a || b = a.
Proof. by case=> [] [] // ->. Qed.
Lemma orb_id2l : forall a b c : bool, (~~ a -> b = c) -> a || b = a || c.
Proof. by case=> [] [] [] // ->. Qed.
Lemma orb_id2r : forall a b c : bool, (~~ b -> a = c) -> a || b = c || b.
Proof. by move=> [] [] [] // ->. Qed.

Lemma negb_and : forall b1 b2, ~~ (b1 && b2) = ~~ b1 || ~~ b2.
Proof. by do 2!case. Qed.

Lemma negb_or : forall b1 b2, ~~ (b1 || b2) = ~~ b1 && ~~ b2.
Proof. by do 2!case. Qed.


Lemma andbK : forall b1 b2, b1 && b2 || b1 = b1. Proof. by do 2!case. Qed.
Lemma andKb : forall b1 b2, b1 || b2 && b1 = b1. Proof. by do 2!case. Qed.
Lemma orbK : forall b1 b2, (b1 || b2) && b1 = b1. Proof. by do 2!case. Qed.
Lemma orKb : forall b1 b2, b1 && (b2 || b1) = b1. Proof. by do 2!case. Qed.


Lemma implybT : forall b, b ==> true. Proof. by case. Qed.
Lemma implybF : forall b, (b ==> false) = ~~ b. Proof. by case. Qed.
Lemma implyFb : forall b, false ==> b. Proof. by []. Qed.
Lemma implyTb : forall b, (true ==> b) = b. Proof. by []. Qed.
Lemma implybb : forall b, b ==> b. Proof. by case. Qed.

Lemma negb_imply : forall b1 b2, ~~ (b1 ==> b2) = b1 && ~~ b2.
Proof. by do 2!case. Qed.

Lemma implybE : forall b1 b2, (b1 ==> b2) = ~~ b1 || b2.
Proof. by do 2!case. Qed.

Lemma implyNb : forall b1 b2, (~~ b1 ==> b2) = b1 || b2.
Proof. by do 2!case. Qed.

Lemma implybN : forall b1 b2, (b1 ==> ~~ b2) = (b2 ==> ~~ b1).
Proof. by do 2!case. Qed.

Lemma implybNN : forall b1 b2, (~~ b1 ==> ~~ b2) = b2 ==> b1.
Proof. by do 2!case. Qed.

Lemma implyb_idl : forall a b : bool, (~~ a -> b) -> (a ==> b) = b.
Proof. by case=> [] [] // ->. Qed.
Lemma implyb_idr : forall a b : bool, (b -> ~~ a) -> (a ==> b) = ~~ a.
Proof. by case=> [] [] // ->. Qed.
Lemma implyb_id2l : forall a b c : bool, (a -> b = c) -> (a ==> b) = (a ==> c).
Proof. by case=> [] [] [] // ->. Qed.


Lemma addFb : left_id false addb. Proof. by []. Qed.
Lemma addbF : right_id false addb. Proof. by case. Qed.
Lemma addbb : self_inverse false addb. Proof. by case. Qed.
Lemma addbC : commutative addb. Proof. by do 2!case. Qed.
Lemma addbA : associative addb. Proof. by do 3!case. Qed.
Lemma addbCA : left_commutative addb. Proof. by do 3!case. Qed.
Lemma addbAC : right_commutative addb. Proof. by do 3!case. Qed.
Lemma andb_addl : left_distributive andb addb. Proof. by do 3!case. Qed.
Lemma andb_addr : right_distributive andb addb. Proof. by do 3!case. Qed.
Lemma addKb : left_loop id addb. Proof. by do 2!case. Qed.
Lemma addbK : right_loop id addb. Proof. by do 2!case. Qed.
Lemma addIb : left_injective addb. Proof. by do 3!case. Qed.
Lemma addbI : right_injective addb. Proof. by do 3!case. Qed.

Lemma addTb : forall b, true (+) b = ~~ b. Proof. by []. Qed.
Lemma addbT : forall b, b (+) true = ~~ b. Proof. by case. Qed.

Lemma addbN : forall b1 b2, b1 (+) ~~ b2 = ~~ (b1 (+) b2).
Proof. by do 2!case. Qed.
Lemma addNb : forall b1 b2, ~~ b1 (+) b2 = ~~ (b1 (+) b2).
Proof. by do 2!case. Qed.

Lemma addbP : forall b1 b2, b1 (+) b2 -> ~~ b1 = b2.
Proof. by do 2!case. Qed.


Ltac bool_congr :=
  match goal with
  | |- (?X1 && ?X2 = ?X3) => first
  [ symmetry; rewrite -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry
  | case: (X1); [ rewrite ?andTb ?andbT // | by rewrite ?andbF /= ] ]
  | |- (?X1 || ?X2 = ?X3) => first
  [ symmetry; rewrite -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry
  | case: (X1); [ by rewrite ?orbT //= | rewrite ?orFb ?orbF ] ]
  | |- (?X1 (+) ?X2 = ?X3) =>
    symmetry; rewrite -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry
  | |- (~~ ?X1 = ?X2) => congr 1 negb
  end.


Definition pred T := T -> bool.

Identity Coercion fun_of_pred : pred >-> Funclass.

Definition rel T := T -> pred T.

Identity Coercion fun_of_rel : rel >-> Funclass.

Notation xpred0 := (fun _ => false).
Notation xpredT := (fun _ => true).
Notation xpredI := (fun (p1 p2 : pred _) x => p1 x && p2 x).
Notation xpredU := (fun (p1 p2 : pred _) x => p1 x || p2 x).
Notation xpredC := (fun (p : pred _) x => ~~ p x).
Notation xpredD := (fun (p1 p2 : pred _) x => ~~ p2 x && p1 x).
Notation xpreim := (fun f (p : pred _) x => p (f x)).
Notation xrelU := (fun (r1 r2 : rel _) x y => r1 x y || r2 x y).

Section Predicates.

Variables T : Type.

Definition subpred (p1 p2 : pred T) := forall x, p1 x -> p2 x.

Definition subrel (r1 r2 : rel T) := forall x y, r1 x y -> r2 x y.

Definition simpl_pred := simpl_fun T bool.

Definition SimplPred (p : pred T) : simpl_pred := SimplFun p.

Coercion pred_of_simpl (p : simpl_pred) : pred T := p : T -> bool.

Definition pred0 := SimplPred xpred0.
Definition predT := SimplPred xpredT.
Definition predI p1 p2 := SimplPred (xpredI p1 p2).
Definition predU p1 p2 := SimplPred (xpredU p1 p2).
Definition predC p := SimplPred (xpredC p).
Definition predD p1 p2 := SimplPred (xpredD p1 p2).
Definition preim rT f (d : pred rT) := SimplPred (xpreim f d).

Definition simpl_rel := simpl_fun T (pred T).

Definition SimplRel (r : rel T) : simpl_rel := [fun x => r x].

Coercion rel_of_simpl_rel (r : simpl_rel) : rel T := fun x y => r x y.

Definition relU r1 r2 := SimplRel (xrelU r1 r2).

Lemma subrelUl : forall r1 r2, subrel r1 (relU r1 r2).
Proof. by move=> * ? *; apply/orP; left. Qed.

Lemma subrelUr : forall r1 r2, subrel r2 (relU r1 r2).
Proof. by move=> * ? *; apply/orP; right. Qed.

CoInductive mem_pred : Type := Mem of pred T.

Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]).

Structure predType : Type := PredType {
  pred_sort :> Type;
  topred : pred_sort -> pred T;
  _ : {mem | isMem topred mem}
}.

Definition mkPredType pT toP := PredType (exist (@isMem pT toP) _ (erefl _)).

Canonical Structure predPredType := Eval hnf in @mkPredType (pred T) id.
Canonical Structure simplPredType := Eval hnf in mkPredType pred_of_simpl.

Coercion pred_of_mem mp : pred_sort predPredType :=
  let: Mem p := mp in [eta p].

Canonical Structure memPredType := Eval hnf in mkPredType pred_of_mem.

Definition clone_pred U :=
  fun pT & pred_sort pT -> U =>
  fun a mP (pT' := @PredType U a mP) & phant_id pT' pT => pT'.

End Predicates.

Implicit Arguments pred0 [T].
Implicit Arguments predT [T].
Prenex Implicits pred0 predT predI predU predC predD preim relU.

Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E))
  (at level 0, format "[ 'pred' : T | E ]") : fun_scope.
Notation "[ 'pred' x | E ]" := (SimplPred (fun x => E))
  (at level 0, x ident, format "[ 'pred' x | E ]") : fun_scope.
Notation "[ 'pred' x : T | E ]" := (SimplPred (fun x : T => E))
  (at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E))
  (at level 0, x ident, y ident, format "[ 'rel' x y | E ]") : fun_scope.
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E))
  (at level 0, x ident, y ident, only parsing) : fun_scope.

Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id)
  (at level 0, format "[ 'predType' 'of' T ]") : form_scope.


Notation pred_class := (pred_sort (predPredType _)).
Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T.

Definition predArgType := Type.
Identity Coercion sort_of_predArgType : predArgType >-> Sortclass.
Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT.

Notation "{ : T }" := (T%type : predArgType)
  (at level 0, format "{ : T }") : type_scope.


Definition mem T (pT : predType T) : pT -> mem_pred T :=
  nosimpl (let: PredType _ _ (exist mem _) := pT return pT -> _ in mem).
Definition in_mem T x mp := nosimpl pred_of_mem T mp x.

Prenex Implicits mem.

Coercion pred_of_mem_pred T mp := [pred x : T | in_mem x mp].

Definition eq_mem T p1 p2 := forall x : T, in_mem x p1 = in_mem x p2.
Definition sub_mem T p1 p2 := forall x : T, in_mem x p1 -> in_mem x p2.

Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \notin A" := (~~ (x \in A)) : bool_scope.
Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope.
Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B))
  (at level 0, A, B at level 69,
   format "{ '[hv' 'subset' A '/ ' <= B ']' }") : type_scope.
Notation "[ 'mem' A ]" := (pred_of_simpl (pred_of_mem_pred (mem A)))
  (at level 0, only parsing) : fun_scope.
Notation "[ 'rel' 'of' fA ]" := (fun x => [mem (fA x)])
  (at level 0, format "[ 'rel' 'of' fA ]") : fun_scope.
Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B])
  (at level 0, format "[ 'predI' A & B ]") : fun_scope.
Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B])
  (at level 0, format "[ 'predU' A & B ]") : fun_scope.
Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B])
  (at level 0, format "[ 'predD' A & B ]") : fun_scope.
Notation "[ 'predC' A ]" := (predC [mem A])
  (at level 0, format "[ 'predC' A ]") : fun_scope.
Notation "[ 'preim' f 'of' A ]" := (preim f [mem A])
  (at level 0, format "[ 'preim' f 'of' A ]") : fun_scope.

Notation "[ 'pred' x \in A ]" := [pred x | x \in A]
  (at level 0, x ident, format "[ 'pred' x \in A ]") : fun_scope.
Notation "[ 'pred' x \in A | E ]" := [pred x | (x \in A) && E]
  (at level 0, x ident, format "[ 'pred' x \in A | E ]") : fun_scope.
Notation "[ 'rel' x y \in A & B | E ]" :=
  [rel x y | (x \in A) && (y \in B) && E]
  (at level 0, x ident, y ident,
   format "[ 'rel' x y \in A & B | E ]") : fun_scope.
Notation "[ 'rel' x y \in A & B ]" := [rel x y | (x \in A) && (y \in B)]
  (at level 0, x ident, y ident,
   format "[ 'rel' x y \in A & B ]") : fun_scope.
Notation "[ 'rel' x y \in A | E ]" := [rel x y \in A & A | E]
  (at level 0, x ident, y ident,
   format "[ 'rel' x y \in A | E ]") : fun_scope.
Notation "[ 'rel' x y \in A ]" := [rel x y \in A & A]
  (at level 0, x ident, y ident,
   format "[ 'rel' x y \in A ]") : fun_scope.

Section simpl_mem.

Variables (T : Type) (pT : predType T).

Lemma mem_topred : forall (p : pT), mem (topred p) = mem p.
Proof. by rewrite /mem; case: pT => T1 app1 [mem1 /= ->]. Qed.

Lemma topredE : forall x (p : pT), topred p x = (x \in p).
Proof. by move=> *; rewrite -mem_topred. Qed.

Lemma in_simpl : forall x (p : simpl_pred T), (x \in p) = p x.
Proof. by []. Qed.

Lemma simpl_predE : forall (p : pred T), [pred x | p x] =1 p.
Proof. by []. Qed.

Definition inE := (in_simpl, simpl_predE).
Lemma mem_simpl : forall (p : simpl_pred T), mem p = p :> pred T.
Proof. by []. Qed.

Definition memE := mem_simpl.
Lemma mem_mem : forall p : pT, (mem (mem p) = mem p) * (mem [mem p] = mem p).
Proof. by move=> p; rewrite -mem_topred. Qed.

End simpl_mem.

Section RelationProperties.


Variable T : Type.

Variable R : rel T.

Definition total := forall x y, R x y || R y x.
Definition transitive := forall y x z, R x y -> R y z -> R x z.

Definition symmetric := forall x y, R x y = R y x.
Definition antisymmetric := forall x y, R x y && R y x -> x = y.
Definition pre_symmetric := forall x y, R x y -> R y x.

Lemma symmetric_from_pre : pre_symmetric -> symmetric.
Proof. move=> symR x y; apply/idP/idP; exact: symR. Qed.

Definition reflexive := forall x, R x x.
Definition irreflexive := forall x, R x x = false.

Definition left_transitive := forall x y, R x y -> R x =1 R y.
Definition right_transitive := forall x y, R x y -> R^~ x =1 R^~ y.

End RelationProperties.

Lemma rev_trans : forall T (R : rel T),
  transitive R -> transitive (fun x y => R y x).
Proof. by move=> T R trR x y z Ryx Rzy; exact: trR Rzy Ryx. Qed.


Notation Local "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
Notation Local "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
Notation Local "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
Notation Local ph := (phantom _).

Section LocalProperties.

Variables T1 T2 T3 : Type.

Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3).
Notation Local ph := (phantom Prop).

Definition prop_for (x : T1) P & ph {all1 P} := P x.

Lemma forE : forall x P phP, @prop_for x P phP = P x. Proof. by []. Qed.

Definition prop_in1 P & ph {all1 P} :=
  forall x, in_mem x d1 -> P x.

Definition prop_in11 P & ph {all2 P} :=
  forall x y, in_mem x d1 -> in_mem y d2 -> P x y.

Definition prop_in2 P & ph {all2 P} :=
  forall x y, in_mem x d1 -> in_mem y d1 -> P x y.

Definition prop_in111 P & ph {all3 P} :=
  forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d3 -> P x y z.

Definition prop_in12 P & ph {all3 P} :=
  forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d2 -> P x y z.

Definition prop_in21 P & ph {all3 P} :=
  forall x y z, in_mem x d1 -> in_mem y d1 -> in_mem z d2 -> P x y z.

Definition prop_in3 P & ph {all3 P} :=
  forall x y z, in_mem x d1 -> in_mem y d1 -> in_mem z d1 -> P x y z.

Variable f : T1 -> T2.

Definition prop_on1 Pf P & phantom T3 (Pf f) & ph {all1 P} :=
  forall x, in_mem (f x) d2 -> P x.

Definition prop_on2 Pf P & phantom T3 (Pf f) & ph {all2 P} :=
  forall x y, in_mem (f x) d2 -> in_mem (f y) d2 -> P x y.

End LocalProperties.

Definition inPhantom := Phantom Prop.
Definition onPhantom T P (x : T) := Phantom Prop (P x).

Definition bijective_in aT rT (d : mem_pred aT) (f : aT -> rT) :=
  exists2 g, prop_in1 d (inPhantom (cancel f g))
           & prop_on1 d (Phantom _ (cancel g)) (onPhantom (cancel g) f).

Definition bijective_on aT rT (cd : mem_pred rT) (f : aT -> rT) :=
  exists2 g, prop_on1 cd (Phantom _ (cancel f)) (onPhantom (cancel f) g)
           & prop_in1 cd (inPhantom (cancel g f)).

Notation "{ 'for' x , P }" :=
  (prop_for x (inPhantom P))
  (at level 0, format "{ 'for' x , P }") : type_scope.

Notation "{ 'in' d , P }" :=
  (prop_in1 (mem d) (inPhantom P))
  (at level 0, format "{ 'in' d , P }") : type_scope.

Notation "{ 'in' d1 & d2 , P }" :=
  (prop_in11 (mem d1) (mem d2) (inPhantom P))
  (at level 0, format "{ 'in' d1 & d2 , P }") : type_scope.

Notation "{ 'in' d & , P }" :=
  (prop_in2 (mem d) (inPhantom P))
  (at level 0, format "{ 'in' d & , P }") : type_scope.

Notation "{ 'in' d1 & d2 & d3 , P }" :=
  (prop_in111 (mem d1) (mem d2) (mem d3) (inPhantom P))
  (at level 0, format "{ 'in' d1 & d2 & d3 , P }") : type_scope.

Notation "{ 'in' d1 & & d3 , P }" :=
  (prop_in21 (mem d1) (mem d3) (inPhantom P))
  (at level 0, format "{ 'in' d1 & & d3 , P }") : type_scope.

Notation "{ 'in' d1 & d2 & , P }" :=
  (prop_in12 (mem d1) (mem d2) (inPhantom P))
  (at level 0, format "{ 'in' d1 & d2 & , P }") : type_scope.

Notation "{ 'in' d & & , P }" :=
  (prop_in3 (mem d) (inPhantom P))
  (at level 0, format "{ 'in' d & & , P }") : type_scope.

Notation "{ 'on' cd , P }" :=
  (prop_on1 (mem cd) (inPhantom P) (inPhantom P))
  (at level 0, format "{ 'on' cd , P }") : type_scope.

Notation "{ 'on' cd & , P }" :=
  (prop_on2 (mem cd) (inPhantom P) (inPhantom P))
  (at level 0, format "{ 'on' cd & , P }") : type_scope.

Notation "{ 'on' cd , P & g }" :=
  (prop_on1 (mem cd) (Phantom (_ -> Prop) P) (onPhantom P g))
  (at level 0, format "{ 'on' cd , P & g }") : type_scope.

Notation "{ 'in' d , 'bijective' f }" := (bijective_in (mem d) f)
  (at level 0, f at level 8,
   format "{ 'in' d , 'bijective' f }") : type_scope.

Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f)
  (at level 0, f at level 8,
   format "{ 'on' cd , 'bijective' f }") : type_scope.


Section LocalGlobal.

Variables T1 T2 T3 : predArgType.
Variables (D1 : pred T1) (D2 : pred T2) (D3 : pred T3).
Variables (d1 d1' : mem_pred T1) (d2 d2' : mem_pred T2) (d3 d3' : mem_pred T3).
Variables (f f' : T1 -> T2) (g : T2 -> T1) (h : T3).
Variables (P1 : T1 -> Prop) (P2 : T1 -> T2 -> Prop).
Variable P3 : T1 -> T2 -> T3 -> Prop.
Variable Q1 : (T1 -> T2) -> T1 -> Prop.
Variable Q1l : (T1 -> T2) -> T3 -> T1 -> Prop.
Variable Q2 : (T1 -> T2) -> T1 -> T1 -> Prop.

Hypothesis sub1 : sub_mem d1 d1'.
Hypothesis sub2 : sub_mem d2 d2'.
Hypothesis sub3 : sub_mem d3 d3'.

Lemma in1W : {all1 P1} -> {in D1, {all1 P1}}.
Proof. by move=> ? ?. Qed.
Lemma in2W : {all2 P2} -> {in D1 & D2, {all2 P2}}.
Proof. by move=> ? ?. Qed.
Lemma in3W : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}}.
Proof. by move=> ? ?. Qed.

Lemma in1T : {in T1, {all1 P1}} -> {all1 P1}.
Proof. by move=> ? ?; auto. Qed.
Lemma in2T : {in T1 & T2, {all2 P2}} -> {all2 P2}.
Proof. by move=> ? ?; auto. Qed.
Lemma in3T : {in T1 & T2 & T3, {all3 P3}} -> {all3 P3}.
Proof. by move=> ? ?; auto. Qed.

Lemma sub_in1 : forall Ph : ph {all1 P1},
  prop_in1 d1' Ph -> prop_in1 d1 Ph.
Proof. move=> ? allP x; move/sub1; exact: allP. Qed.

Lemma sub_in11 : forall Ph : ph {all2 P2},
  prop_in11 d1' d2' Ph -> prop_in11 d1 d2 Ph.
Proof. move=> ? allP x1 x2; move/sub1=> d1x1; move/sub2; exact: allP. Qed.

Lemma sub_in111 : forall Ph : ph {all3 P3},
  prop_in111 d1' d2' d3' Ph -> prop_in111 d1 d2 d3 Ph.
Proof.
move=> ? allP x1 x2 x3.
move/sub1=> d1x1; move/sub2=> d2x2; move/sub3; exact: allP.
Qed.

Let allQ1 f'' := {all1 Q1 f''}.
Let allQ1l f'' h' := {all1 Q1l f'' h'}.
Let allQ2 f'' := {all2 Q2 f''}.

Lemma on1W : allQ1 f -> {on D2, allQ1 f}. Proof. by move=> ? ?. Qed.

Lemma on1lW : allQ1l f h -> {on D2, allQ1l f & h}. Proof. by move=> ? ?. Qed.

Lemma on2W : allQ2 f -> {on D2 &, allQ2 f}. Proof. by move=> ? ?. Qed.

Lemma on1T : {on T2, allQ1 f} -> allQ1 f. Proof. by move=> ? ?; auto. Qed.

Lemma on1lT : {on T2, allQ1l f & h} -> allQ1l f h.
Proof. by move=> ? ?; auto. Qed.

Lemma on2T : {on T2 &, allQ2 f} -> allQ2 f.
Proof. by move=> ? ?; auto. Qed.

Lemma subon1 : forall (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)),
  prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.
Proof. move=> ? ? allQ x; move/sub2; exact: allQ. Qed.

Lemma subon1l : forall (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)),
  prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.
Proof. move=> ? ? allQ x; move/sub2; exact: allQ. Qed.

Lemma subon2 : forall (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)),
  prop_on2 d2' Phf Ph -> prop_on2 d2 Phf Ph.
Proof. move=> ? ? allQ x y; move/sub2=> d2fx; move/sub2; exact: allQ. Qed.

Lemma can_in_inj : {in D1, cancel f g} -> {in D1 &, injective f}.
Proof.
by move=> fK x y; do 2![move/fK=> def; rewrite -{2}def {def}] => ->.
Qed.

Lemma canLR_in : forall x y,
  {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y.
Proof. by move=> x y fK D1y ->; rewrite fK. Qed.

Lemma canRL_in : forall x y,
  {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y.
Proof. by move=> x y fK D1x <-; rewrite fK. Qed.

Lemma on_can_inj : {on D2, cancel f & g} -> {on D2 &, injective f}.
Proof.
by move=> fK x y; do 2![move/fK=> def; rewrite -{2}def {def}] => ->.
Qed.

Lemma canLR_on : forall x y,
  {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y.
Proof. by move=> x y fK D2fy ->; rewrite fK. Qed.

Lemma canRL_on : forall x y,
  {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y.
Proof. by move=> x y fK D2fx <-; rewrite fK. Qed.

Lemma inW_bij : bijective f -> {in D1, bijective f}.
Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.

Lemma onW_bij : bijective f -> {on D2, bijective f}.
Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.

Lemma inT_bij : {in T1, bijective f} -> bijective f.
Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.

Lemma onT_bij : {on T2, bijective f} -> bijective f.
Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed.

Lemma sub_in_bij : forall D1' : pred T1,
  {subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f}.
Proof.
move=> D1' subD [g' fK g'K].
exists g' => x; move/subD; [exact: fK | exact: g'K].
Qed.

Lemma subon_bij : forall D2' : pred T2,
 {subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f}.
Proof.
move=> D2' subD [g' fK g'K].
exists g' => x; move/subD; [exact: fK | exact: g'K].
Qed.

End LocalGlobal.

Lemma sub_in2 : forall T d d' (P : T -> T -> Prop),
  sub_mem d d' -> forall Ph : ph {all2 P}, prop_in2 d' Ph -> prop_in2 d Ph.
Proof. by move=> T d d' P /= sub; exact: sub_in11. Qed.

Lemma sub_in3 : forall T d d' (P : T -> T -> T -> Prop),
  sub_mem d d' -> forall Ph : ph {all3 P}, prop_in3 d' Ph -> prop_in3 d Ph.
Proof. by move=> T d d' P /= sub; exact: sub_in111. Qed.

Lemma sub_in12 : forall T1 T d1 d1' d d' (P : T1 -> T -> T -> Prop),
  sub_mem d1 d1' -> sub_mem d d' ->
  forall Ph : ph {all3 P}, prop_in12 d1' d' Ph -> prop_in12 d1 d Ph.
Proof. by move=> T1 T d1 d1' d d' P /= sub1 sub; exact: sub_in111. Qed.

Lemma sub_in21 : forall T T3 d d' d3 d3' (P : T -> T -> T3 -> Prop),
  sub_mem d d' -> sub_mem d3 d3' ->
  forall Ph : ph {all3 P}, prop_in21 d' d3' Ph -> prop_in21 d d3 Ph.
Proof. by move=> T T3 d d' d3 d3' P /= sub sub3; exact: sub_in111. Qed.