CPPsiteProjPackage.CPP_genT


(* general purpose stuff, using Type rather than Prop *)

Set Implicit Arguments.
Require Import List.
Import ListNotations.
Require Import CPP_existsT.

Require Export Coq.Classes.CRelationClasses.

Require Import CPP_gen.

Polymorphic Definition rlsT W := list W W Type.

(* how to express the empty set *)
Inductive emptyT {X : Type} : X Type := .

Lemma emptyT_any': (sty : Type) Q (prem : sty), emptyT prem Q prem.
Proof. intros. induction H. Qed.

Lemma emptyT_any: (sty : Type) Q (prem : sty), emptyT prem Q.
Proof. intros. induction H. Qed.

(* compare 
  https://coq.inria.fr/stdlib/Coq.Relations.Relation_Definitions.html *)

Polymorphic Definition relationT (A : Type) := A A Type.
Inductive empty_relT {A B : Type} : A B Type := .

Lemma rsub_emptyT {A B} r : @rsub A B empty_relT r.
Proof. intros u v e. destruct e. Qed.

Definition transitiveT W (R : relationT W) :=
   (x y z : W), R x y R y z R x z.

(*
Definition iffT A B : Type := (A -> B) * (B -> A).
*)

Lemma iffT_trans: A B C, iffT A B iffT B C iffT A C.
Proof. unfold iffT. intros. destruct X. destruct . tauto. Qed.

Lemma iffT_sym': A B, iffT A B iffT B A.
Proof. unfold iffT. intros. destruct X. tauto. Qed.

Lemma iffT_refl: A, iffT A A.
Proof. unfold iffT. intros. tauto. Qed.

Lemma iffT_D1': A B, iffT A B A B.
Proof. unfold iffT. intros. tauto. Qed.

Lemma iffT_D2': A B, iffT B A A B.
Proof. unfold iffT. intros. tauto. Qed.

(* simpler proof objects *)
Definition iffT_sym (A B : Type) (X : iffT A B) := let (f, g) := X in (g, f).
Definition iffT_D1 (A B : Type) (X : iffT A B) a := let (f, _) := X in f a.
Definition iffT_D2 (A B : Type) (X : iffT A B) b := let (_, g) := X in g b.

Lemma prod_mono A A' B B' : (A A') (B B') (A * B A' * B').
Proof. intros. destruct . tauto. Qed.

Lemma iffT_prod A A' B B' : iffT A A' iffT B B' iffT (A * B) ( A' * B').
Proof. unfold iffT. intros. destruct X. destruct .
split ; apply prod_mono ; assumption. Qed.


(* or defined versions of these
Definition prod_mono_d A A' B B' aa bb (ab : A * B) :=
  let (a, b) := ab in (aa a : A', bb b : B').

Definition iffT_prod_d A A' B B' (iaa : iffT A A') (ibb : iffT B B') :=
  let (af, ab) := iaa in 
    let (bf, bb) := ibb in (prod_mono af bf, prod_mono ab bb).
*)


Inductive AccT (A : Type) (R : A A Type) (x : A) : Type :=
    AccT_intro : ( y : A, R y x AccT R y) AccT R x.

Definition well_foundedT (A : Type) (R : A A Type) :=
   a : A, AccT R a.

Inductive ForallT (A : Type) (P : A Type) : list A Type :=
    ForallT_nil : ForallT P []
  | ForallT_cons : (x : A) (l : list A),
                  P x ForallT P l ForallT P (x :: l).

Lemma ForallT_inv:
   (A : Type) (P : A Type) (a : A) (l : list A),
  ForallT P (a :: l) P a.
Proof. intros. inversion X. subst. exact . Qed.

Lemma ForallT_cons_inv:
   (A : Type) (P : A Type) (x : A) (l : list A),
  ForallT P (x :: l) P x * ForallT P l.
Proof. intros. inversion X. subst. split. exact . exact . Qed.

Lemma ForallT_single:
   (A : Type) (P : A Type) (x : A), iffT (ForallT P [x]) (P x).
Proof. intros. unfold iffT. split ; intros.
  inversion X. subst. exact .
  apply ForallT_cons. exact X. apply ForallT_nil. Qed.


Definition ForallT_singleD A P x := iffT_D1 (@ForallT_single A P x).
Definition ForallT_singleI A P x := iffT_D2 (@ForallT_single A P x).

Lemma ForallT_cons_iff:
   (A : Type) (P : A Type) (x : A) (l : list A),
    iffT (ForallT P (x :: l)) (P x * ForallT P l).
Proof. intros. unfold iffT. split ; intros.
  apply ForallT_cons_inv. exact X.
  destruct X. apply ForallT_cons. exact p. exact f. Qed.


Lemma ForallT_append:
   (X : Type) (P : X Type) (xs ys : list X),
  iffT (ForallT P (xs ys)) (ForallT P xs * ForallT P ys).
Proof. intros. unfold iffT.
  induction xs. simpl. split ; intros. split.
  apply ForallT_nil. exact . destruct . exact .
  destruct IHxs. split ; intros.
  simpl in . inversion . subst. apply p in . destruct .
  split. apply ForallT_cons ; assumption. assumption.
  simpl. destruct . inversion . subst.
  apply ForallT_cons. exact . apply f. split ; assumption. Qed.


Definition ForallT_appendD A P xs ys := iffT_D1 (@ForallT_append A P xs ys).
Definition ForallT_appendD1 A P xs ys aa := fst (@ForallT_appendD A P xs ys aa).
Definition ForallT_appendD2 A P xs ys aa := snd (@ForallT_appendD A P xs ys aa).
Definition ForallT_appendI' A P xs ys := iffT_D2 (@ForallT_append A P xs ys).
Definition ForallT_appendI A P xs ys ax ay :=
  @ForallT_appendI' A P xs ys (pair ax ay).

Lemma ForallT_2: (A : Type) (P : A Type) (x y : A),
      iffT (ForallT P [x; y]) (P x * P y).
Proof. intros. unfold iffT. split ; intros.
inversion X. subst. inversion . subst. tauto.
destruct X. apply ForallT_cons. exact p.
apply ForallT_cons. exact . apply ForallT_nil. Qed.


Lemma ForallT_map_2: (A B : Type) (P : B Type) (f : A B) (x y : A),
      iffT (ForallT P (map f [x; y])) (P (f x) * P (f y)).
Proof. intros. simpl. apply ForallT_2. Qed.

Lemma ForallT_map: (A B : Type) (P : B Type) (f : A B) (x : A),
      iffT (ForallT P (map f [x])) (P (f x)).
Proof. intros. simpl. apply ForallT_single. Qed.

Lemma ForallT_map_rev: (A B : Type) (P : B Type) (f : A B) (x : A),
      iffT (P (f x)) (ForallT P (map f [x])).
Proof. intros. simpl. split; intros HH; apply ForallT_single; tauto. Qed.

Definition ForallT_2D A P x y := iffT_D1 (@ForallT_2 A P x y).
Definition ForallT_D1 A P x y aa := fst (@ForallT_2D A P x y aa).
Definition ForallT_D2 A P x y aa := snd (@ForallT_2D A P x y aa).
Definition ForallT_2I' A P x y := iffT_D2 (@ForallT_2 A P x y).
Definition ForallT_2I A P x y ax ay := @ForallT_2I' A P x y (pair ax ay).

Lemma ForallT_impl:
   (A : Type) (P Q : A Type),
  ( a : A, P a Q a) l : list A, ForallT P l ForallT Q l.
Proof. intros. induction . apply ForallT_nil.
  apply ForallT_cons. apply X. apply p. assumption. Qed.


(*
ForallT_Exists_neg:
  forall (A : Type) (P : A -> Prop) (l : list A),
  ForallT (fun x : A => ~ P x) l <-> ~ Exists P l
ForallT_dec:
  forall (A : Type) (P : A -> Prop),
  (forall x : A, {P x} + {~ P x}) ->
  forall l : list A, {ForallT P l} + {~ ForallT P l}
ForallT_map_single:
  forall (A B : Type) (P : B -> Prop) (f : A -> B) (x : A),
  ForallT P (map f x) <-> P (f x)
*)


Inductive Forall2T (A B : Type) R : list A list B Type :=
    Forall2T_nil : Forall2T R [] []
  | Forall2T_cons : (x : A) (y : B) (l : list A) (l' : list B),
                   R x y Forall2T R l l' Forall2T R (x :: l) (y :: l')
  .

Theorem Forall2T_app_inv_l : A B (R : A B Type) l1 l2 l',
  Forall2T R ( ) l'
   (fun l1' Forall2T R ) (fun l1' (fun l2'
    Forall2T R ) (fun l2' l' = )).
Proof. intros until . induction . simpl.
intros. exists []. apply Forall2T_nil.
exists l'. assumption. simpl. reflexivity.
simpl. intros. inversion_clear X.
apply in . destruct .
exists (y :: x). apply Forall2T_cons ; assumption.
destruct s. subst. simpl. eexists. eassumption. reflexivity. Qed.


Theorem Forall2T_app_inv_r : A B (R : A B Type) l1' l2' l,
  Forall2T R l ( )
   (fun l1 Forall2T R ) (fun l1 (fun l2
    Forall2T R ) (fun l2 l = )).
Proof. intros until . induction . simpl.
intros. exists []. apply Forall2T_nil.
exists l. assumption. simpl. reflexivity.
simpl. intros. inversion_clear X.
apply in . destruct .
exists (x :: ). apply Forall2T_cons ; assumption.
destruct s. subst. simpl. eexists. eassumption. reflexivity. Qed.


Theorem Forall2T_app : A B (R : A B Type) l1 l2 l1' l2',
  Forall2T R Forall2T R Forall2T R ( ) ( ).
Proof. intros until . induction . simpl.
intros. inversion_clear X. simpl. assumption.
intros. inversion_clear X. simpl. apply Forall2T_cons. assumption.
apply ; assumption. Qed.


(* this isn't usable, because destruct doesn't work for first clause 
Inductive InT A (a : A) : list A -> Type :=
  | InT_eq : forall l, @InT A a (a :: l)
  | InT_cons : forall b l, @InT A a l -> @InT A a (b :: l).
 *)

  Ltac cET :=
  repeat match goal with
    | [ H : _ _ |- _ ] inversion_clear H
    | [ H : ex _ |- _ ] inversion_clear H
    | [ H : False |- _ ] contradiction H
    | [ H : sig _ |- _ ] inversion_clear H
    | [ H : sigT _ |- _ ] inversion_clear H
    | [ H : False |- _ ] contradiction H
    | [ H : _ * _ |- _ ] inversion_clear H
         end.

  Ltac cET_nr :=
  match goal with
    | [ H : _ _ |- _ ] inversion_clear H
    | [ H : ex _ |- _ ] inversion_clear H
    | [ H : False |- _ ] contradiction H
    | [ H : sig _ |- _ ] inversion_clear H
    | [ H : sigT _ |- _ ] inversion_clear H
    | [ H : False |- _ ] contradiction H
    | [ H : _ * _ |- _ ] inversion_clear H
    end.

Inductive InT A (a : A) : list A Type :=
  | InT_eq' : b l, b = a @InT A a (b :: l)
  | InT_cons : b l, @InT A a l @InT A a (b :: l).

Lemma InT_eq: A a l, @InT A a (a :: l).
Proof. intros. apply InT_eq'. reflexivity. Qed.

Definition InT_2nd A (a b : A) l := InT_cons a (InT_eq b l).

Lemma InT_appL: A a X Y, InT (a : A) X InT a (X Y).
Proof. intros. induction ; simpl. subst.
apply InT_eq. apply InT_cons. assumption. Qed.


Lemma InT_appR: A a X Y, InT (a : A) Y InT a (X Y).
Proof. intros. induction X ; simpl. assumption.
apply InT_cons. assumption. Qed.


Ltac solve_InT := apply InT_eq ||
  ((apply InT_cons || (apply InT_appL + apply InT_appR)) ; solve_InT).

Lemma InT_appE': A a Z, InT (a : A) Z
   X Y, Z = X Y InT a X + InT a Y.
Proof. intros until 0. intro. induction X ; intros.
destruct X ; simpl in H. subst. right. apply InT_eq.
injection H. intros. subst. left. apply InT_eq.
destruct ; simpl in H. subst. right. apply InT_cons. assumption.
injection H. intros. subst. pose (@eq_refl (list A)). apply IHX in e.
destruct e. left. apply InT_cons. assumption.
right. assumption. Qed.


Lemma InT_appE: A a X Y, InT (a : A) (X Y) InT a X + InT a Y.
Proof. intros. eapply InT_appE'. eassumption. reflexivity. Qed.

Lemma InT_nilE': A a Z any, InT (a : A) Z Z = [] any.
Proof. intros. induction X ; discriminate. Qed.

Lemma InT_nilE: A a any, InT (a : A) [] any.
Proof. intros. eapply InT_nilE'. eassumption. reflexivity. Qed.

Lemma InT_split: (A : Type) (x : A) (l : list A),
  InT x l sigT (fun l1 sigT (fun l2 l = x :: )).
Proof. intros. induction X.
exists []. exists l. simpl. subst. reflexivity.
destruct IHX. destruct s. subst.
exists (b :: ). exists . simpl. reflexivity. Qed.


Lemma InT_inv: A a b Y, InT (a : A) (b :: Y) (b = a) + InT a Y.
Proof. intros. inversion X ; subst ; tauto. Qed.

Lemma InT_map: (A B : Type) (f : A B) (l : list A) (x : A),
  InT x l InT (f x) (map f l).
Proof. intros. induction X.
subst. simpl. apply InT_eq.
simpl. apply InT_cons. assumption. Qed.


Lemma InT_mapE: (A B : Type) (f : A B) (l : list A) (y : B),
       (InT y (map f l)) (sigT (fun x prod (f x = y) (InT x l))).
Proof. intros.
induction l. eapply InT_nilE in X. apply X.
simpl in X. inversion X. subst. exists a.
split. reflexivity. apply InT_eq.
subst. apply IHl in . cD. exists . subst. split. reflexivity.
apply InT_cons. exact . Qed.


Lemma InT_map_iffT: (A B : Type) (f : A B) (l : list A) (y : B),
       iffT (InT y (map f l)) (sigT (fun x prod (f x = y) (InT x l))).
Proof. intros. apply pair. apply InT_mapE.
intro. cD. subst. apply InT_map. exact . Qed.


Definition InT_mapI A B f l y := iffT_D2 (@InT_map_iffT A B f l y).

Lemma InT_concat: (A : Type) a (xs : list A) pss,
     InT a xs InT xs pss InT a (concat pss).
Proof. intros. induction . subst. simpl. apply InT_appL. assumption.
simpl. apply InT_appR. assumption. Qed.


Lemma Forall2T_ex_l: A B (R : A B Type) xs ys x,
  Forall2T R xs ys InT x xs (fun y InT y ys) (fun y R x y).
Proof. intros until 0. intro. induction X.
intro. eapply InT_nilE in X. eassumption.
intro. inversion ; subst. eexists. apply InT_eq. assumption.
apply IHX in . destruct . eexists. eapply InT_cons. eassumption.
assumption. Qed.


Lemma Forall2T_ex_r: A B (R : A B Type) xs ys x,
  Forall2T R ys xs InT x xs (fun y InT y ys) (fun y R y x).
Proof. intros until 0. intro. induction X.
intro. eapply InT_nilE in X. eassumption.
intro. inversion ; subst. eexists. apply InT_eq. assumption.
apply IHX in . destruct . eexists. eapply InT_cons. eassumption.
assumption. Qed.


Lemma ForallT_forall: (A : Type) (P : A Type) (l : list A),
  iffT (ForallT P l) ( x : A, InT x l P x).
Proof. intros. induction l ; unfold iffT ; split ; intros.
  eapply InT_nilE in . exact . apply ForallT_nil.
  unfold iffT in IHl. destruct IHl. inversion X.
  inversion ; subst ; firstorder.
  unfold iffT in IHl. destruct IHl.
  apply ForallT_cons. apply X. apply InT_eq.
  apply f. intros. apply X. apply InT_cons. exact . Qed.


Definition ForallTD_forall A P x := iffT_D1 (@ForallT_forall A P x).
Definition ForallTI_forall A P x := iffT_D2 (@ForallT_forall A P x).

Lemma InT_In: A a Y, InT (a : A) Y In a Y.
Proof. intros. induction X. subst. apply in_eq.
apply in_cons. assumption. Qed.


Lemma In_InT: A a Y, In (a : A) Y ex (fun _ : InT a Y True).
Proof. intros. induction Y. apply in_nil in H. contradiction.
apply in_inv in H. destruct H. subst. exists. apply InT_eq. apply I.
apply IHY in H. destruct H. exists. apply InT_cons. assumption. apply I. Qed.


(* generalise this *)
Definition anon (p : Type) := ex (fun _ : p True).

Lemma anonI : p, p anon p.
Proof. intros. unfold anon. exists. assumption. apply I. Qed.

Lemma InT_In': A a Y, ex (fun _ : InT (a : A) Y True) In a Y.
Proof. intros. destruct H. apply InT_In. assumption. Qed.
(* why can't we do anon p -> p in general, we do it here?
  note, trying apply InT_In. before destruct H. causes the error below *)


(*
Lemma anonD : forall p, anon p -> p.
Proof. unfold anon. intros. destruct H.
Error: Case analysis on sort Type is not allowed for inductive definition ex.
*)

Lemma anonD : p (q : Prop), (p q) (anon p q).
Proof. unfold anon. intros. destruct . tauto. Qed.

Lemma anon_eq: P : Prop, anon P P.
Proof. intros. unfold iff. split. apply anonD. tauto. apply anonI. Qed.

Lemma InT_In_eq: A a Y, anon (InT (a : A) Y) In a Y.
Proof. unfold anon. intros. unfold iff. split ; intros.
apply InT_In'. assumption. apply In_InT. assumption. Qed.


Lemma InT_In_eq': A a Y, anon (InT (a : A) Y) In a Y.
Proof. intros. unfold iff. split.
apply anonD. apply InT_In.
intro. unfold anon. apply In_InT. assumption. Qed.


Lemma anon_prod: t u, anon (prod t u) anon t anon u.
Proof. intros. unfold iff. unfold anon. split ; intros ;
  cD ; try split ; exists ; tauto. Qed.


Lemma anon_sum: t u, anon (sum t u) anon t anon u.
Proof. intros. unfold iff. unfold anon. split ; intros ; sD ;
  [> left | right | | ] ; exists ; tauto. Qed.


(* doubt if converse is valid *)
Lemma anon_imp: t u, anon (t u) (anon t anon u).
Proof. unfold anon. intros. cD. exists ; tauto. Qed.

Lemma anon_iffT: t u, anon (iffT t u) (anon t anon u).
Proof. unfold iff. unfold iffT. intros.
rewrite anon_prod in H. destruct H.
split ; intros ; eapply anon_imp ; eassumption. Qed.


Lemma anon_sigT: A P, anon (@sigT A P) @ex A (fun x anon (P x)).
Proof. unfold anon. intros. cD. eexists. eexists. eassumption. apply I. Qed.

Lemma anon_forall: T P,
  anon ( x : T, P x) x : T, anon (P x).
Proof. unfold anon. intros. destruct H. exists. apply ( x). apply I. Qed.

(* example to use the above - to prove in_inv 
Goal forall (A : Type) (a b : A) l, In b (a :: l) -> a = b \/ In b l.
Proof.  intros.  pose InT_inv.
apply anonI in s.
eapply anon_forall in s.
eapply anon_forall in s.
eapply anon_forall in s.
eapply anon_forall in s.
eapply anon_imp in s. (* this doesn't work as I'd expect *)
Undo.
pose anon_imp.
pose (a0 (InT ?x0 (?x1 :: ?x2)) (?x1 = ?x0) + InT ?x0 ?x2). (* fails *)
*)


Lemma ForallT_Forall': A (P : A Prop) (xs : list A),
  ForallT P xs Forall P xs.
Proof. intros. induction X. apply Forall_nil.
apply Forall_cons. assumption. assumption. Qed.


Lemma ForallT_Forall: A P (xs : list A),
  ForallT P xs Forall (fun x anon (P x)) xs.
Proof. intros. induction X. apply Forall_nil.
apply Forall_cons. apply anonI. assumption. assumption. Qed.


Lemma Forall_ForallT: A P (xs : list A),
  Forall P xs anon (ForallT P xs).
Proof. intros. induction H. apply anonI. apply ForallT_nil.
unfold anon in IHForall. cD. apply anonI. (* can't do this before cD *)
apply ForallT_cons ; assumption. Qed.


(* note proof carefully, intros then induction H fails,
  inversion H too early fails *)

Lemma Forall_ForallT': A P (xs : list A), Forall P xs ForallT P xs.
Proof. intros. induction xs. apply ForallT_nil.
apply ForallT_cons. inversion H. subst. assumption.
apply IHxs. inversion H. subst. assumption.
Qed.


Lemma inhabited_anon: A, inhabited A anon A.
Proof. unfold iff. unfold anon. intros. split ; intros.
 destruct H. exists ; tauto.
 destruct H. apply inhabits. assumption. Qed.


Lemma want_left_prod_under_universal : (T : Type) (P : T Type) (Q1 : T Type) (S : Type),
    ( y : T, P y (( y) * S))
     y : T, P y y.
Proof. firstorder. Qed.

Lemma want_right_prod_under_universal : (T : Type) (P : T Type) (Q1 : T Type) (S : Type),
    ( y : T, P y (S * ( y)))
     y : T, P y y.
Proof. firstorder. Qed.

Lemma want_right_prod_under_universal' : (T : Type) (P : T Type) (Q1 S : T Type),
    ( y : T, P y ((S y) * ( y)))
     y : T, P y y.
Proof. firstorder. Qed.

Lemma want_prod_under_universal4 : (T : Type) (P : T Type) (Q1 Q2 Q3 Q4 : T Type),
    ( y : T, P y (( y) * ( y) * ( y) * ( y)))
    ( y : T, P y y) *
    ( y : T, P y y) *
    ( y : T, P y y) *
    ( y : T, P y y).
Proof. firstorder. Qed.

Lemma prod_nat_split : (P : ( * ) Type),
    ( y : * , P y)
    ( n m : , P (n,m)).
Proof. firstorder. Qed.

Inductive empty : Type := .

Lemma empty_explosion : (A : Type), empty A.
Proof. intros A H. inversion H. Qed.

Notation "T~ A" := (A empty) (at level 60).

Lemma False_empty : False empty.
Proof. intros H. inversion H. Qed.

Lemma empty_False : empty False.
Proof. intros H. inversion H. Qed.

Inductive leT (n : ) : Type :=
  | leT_n : leT n n | leT_S : m : , leT n m leT n (S m).

Theorem leT_n_S : n m, leT n m leT (S n) (S m).
Proof. intros. induction H. apply leT_n. apply (leT_S IHleT). Qed.

Lemma leT_S_n' : sn sm, leT sn sm
   n m, sn = S n sm = S m leT n m.
Proof. intros * ss. induction ss.
- intros. subst. inversion . apply leT_n.
- destruct m.
+ inversion ss. intros. inversion .
+ intros. subst. specialize (IHss _ _ eq_refl eq_refl).
inversion . exact (leT_S IHss). Qed.


(* forall n m, leT (S n) (S m) -> leT n m *)
Definition leT_S_n n m l := @leT_S_n' _ _ l n m eq_refl eq_refl.

Lemma leT_trans' l m n: leT m n leT l m leT l n.
Proof. intro. induction H ; intro. apply H. exact (leT_S (IHleT )). Qed.

Definition leT_trans l m n llm lmn := @leT_trans' l m n lmn llm.

Lemma leT_0_n n: leT 0 n.
Proof. induction n. apply leT_n. apply (leT_S IHn). Qed.

Lemma leT_plus_r n m : leT m (n + m).
Proof. induction n ; simpl. apply leT_n. apply (leT_S IHn). Qed.

Lemma leT_plus_l n m : leT n (n + m).
Proof. induction n ; simpl. apply leT_0_n. apply (leT_n_S IHn). Qed.

Theorem eq_S_F n : S n = n False.
Proof. intro. induction n ; inversion H. tauto. Qed.

Theorem leT_S_F n : leT (S n) n False.
Proof. induction n ; intro. inversion H. apply leT_S_n in H. tauto. Qed.

Lemma leT_S_or_eq n m : leT n m leT (S n) m + (n = m).
Proof. intro. induction H. tauto. left. exact (leT_n_S H). Qed.

Lemma leT_or_gt n m : leT n m + leT (S m) n.
Proof. induction n. left. apply leT_0_n.
destruct IHn. apply leT_S_or_eq in l. destruct l. exact (inl l).
subst. exact (inr (leT_n _)). exact (inr (leT_S l)). Qed.


Lemma leT_ex_plus k n : leT k n { m : & Nat.add m k = n }.
Proof. intro lkn. induction lkn. exists 0. simpl. reflexivity.
cD. subst. exists (S IHlkn). simpl. reflexivity. Qed.