Recover the contra lemmas

syntax.sig

@@ -14,3 +14,4 @@ Proj : PTag -> Tm -> Tm
 TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
 Const : TTag -> Tm
 Univ : nat -> Tm
+Bot : Tm

theories/Autosubst2/syntax.v

@@ -41,7 +41,8 @@ Inductive Tm (n_Tm : nat) : Type :=
   | Proj : PTag -> Tm n_Tm -> Tm n_Tm
   | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm
   | Const : TTag -> Tm n_Tm
-  | Univ : nat -> Tm n_Tm.
+  | Univ : nat -> Tm n_Tm
+  | Bot : Tm n_Tm.
 
 Lemma congr_Abs {m_Tm : nat} {s0 : Tm (S m_Tm)} {t0 : Tm (S m_Tm)}
   (H0 : s0 = t0) : Abs m_Tm s0 = Abs m_Tm t0.
@@ -95,6 +96,11 @@ Proof.
 exact (eq_trans eq_refl (ap (fun x => Univ m_Tm x) H0)).
 Qed.
 
+Lemma congr_Bot {m_Tm : nat} : Bot m_Tm = Bot m_Tm.
+Proof.
+exact (eq_refl).
+Qed.
+
 Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) :
   fin (S m) -> fin (S n).
 Proof.
@@ -119,6 +125,7 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
       TBind n_Tm s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2)
   | Const _ s0 => Const n_Tm s0
   | Univ _ s0 => Univ n_Tm s0
+  | Bot _ => Bot n_Tm
   end.
 
 Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
@@ -146,6 +153,7 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
       TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2)
   | Const _ s0 => Const n_Tm s0
   | Univ _ s0 => Univ n_Tm s0
+  | Bot _ => Bot n_Tm
   end.
 
 Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
@@ -186,6 +194,7 @@ subst_Tm sigma_Tm s = s :=
         (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -230,6 +239,7 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
            (upExtRen_Tm_Tm _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
@@ -275,6 +285,7 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
            s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -320,6 +331,7 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
            (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
@@ -376,6 +388,7 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
            (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -453,6 +466,7 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
            (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -531,6 +545,7 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
            (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
@@ -647,6 +662,7 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
            (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2)
   | Const _ s0 => congr_Const (eq_refl s0)
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bot _ => congr_Bot
   end.
 
 Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
@@ -845,6 +861,8 @@ Core.
 
 Arguments VarTm {n_Tm}.
 
+Arguments Bot {n_Tm}.
+
 Arguments Univ {n_Tm}.
 
 Arguments Const {n_Tm}.

theories/compile.v

@@ -13,6 +13,7 @@ Module Compile.
     | VarTm i => VarTm i
     | Pair a b => Pair (F a) (F b)
     | Proj t a => Proj t (F a)
+    | Bot => Bot
     end.
 
   Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :

theories/fp_red.v

@@ -72,7 +72,9 @@ Module Par.
   | ConstCong k :
     R (Const k) (Const k)
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BotCong :
+    R Bot Bot.
 
   Lemma refl n (a : Tm n) : R a a.
     elim : n /a; hauto ctrs:R.
@@ -134,6 +136,7 @@ Module Par.
     - hauto l:on inv:option ctrs:R use:renaming.
     - sfirstorder.
     - sfirstorder.
+    - sfirstorder.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -213,6 +216,7 @@ Module Par.
       by asimpl.
     - move => n k m ξ []//=. hauto l:on.
     - move => n i n0 ξ []//=. hauto l:on.
+    - hauto q:on inv:Tm ctrs:R.
   Qed.
 
 End Par.
@@ -277,7 +281,7 @@ End Pars.
 Definition var_or_const {n} (a : Tm n) :=
   match a with
   | VarTm _ => true
-  | Const _ => true
+  | Bot => true
   | _ => false
   end.
 
@@ -326,7 +330,9 @@ Module RPar.
   | ConstCong k :
     R (Const k) (Const k)
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BotCong :
+    R Bot Bot.
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
@@ -394,6 +400,7 @@ Module RPar.
     - hauto lq:on ctrs:R use:morphing_up.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -533,6 +540,7 @@ Module RPar.
     - hauto q:on ctrs:R inv:Tm.
     - move => n i n0 ρ hρ []//=; first by antiimp.
       hauto l:on.
+    - move => n m ρ hρ []//=; hauto lq:on ctrs:R.
   Qed.
 End RPar.
 
@@ -573,7 +581,9 @@ Module RPar'.
   | ConstCong k :
     R (Const k) (Const k)
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BotCong :
+    R Bot Bot.
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
@@ -639,6 +649,7 @@ Module RPar'.
     - hauto lq:on ctrs:R use:morphing_up.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -758,6 +769,7 @@ Module RPar'.
     - hauto q:on ctrs:R inv:Tm.
     - move => n i n0 ρ hρ []//=; first by antiimp.
       hauto l:on.
+    - hauto q:on inv:Tm ctrs:R.
   Qed.
 End RPar'.
 
@@ -896,7 +908,9 @@ Module EPar.
   | ConstCong k :
     R (Const k) (Const k)
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BotCong :
+    R Bot Bot.
 
   Lemma refl n (a : Tm n) : EPar.R a a.
   Proof.
@@ -941,6 +955,7 @@ Module EPar.
     - hauto l:on ctrs:R use:renaming inv:option.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n a0 a1 (b0 b1 : Tm n) :
@@ -1344,6 +1359,7 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong.
   - hauto l:on ctrs:EPar.R inv:RPar.R.
   - hauto l:on ctrs:EPar.R inv:RPar.R.
+  - hauto l:on ctrs:EPar.R inv:RPar.R.
 Qed.
 
 Lemma commutativity1 n (a b0 b1 : Tm n) :
@@ -1457,6 +1473,20 @@ Lemma Const_EPar' n k (u : Tm n) :
   - hauto l:on ctrs:OExp.R.
 Qed.
 
+Lemma Bot_EPar' n (u : Tm n) :
+  EPar.R (Bot) u ->
+  rtc OExp.R (Bot) u.
+  move E : (Bot) => t h.
+  move : E. elim : n t u /h => //=.
+  - move => n a0 a1 h ih ?. subst.
+    specialize ih with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - move => n a0 a1 h ih ?. subst.
+    specialize ih with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - hauto l:on ctrs:OExp.R.
+Qed.
+
 Lemma Univ_EPar' n i (u : Tm n) :
   EPar.R (Univ i) u ->
   rtc OExp.R (Univ i) u.
@@ -1520,6 +1550,7 @@ Proof.
     exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
   - qauto use:Const_EPar', EPar.refl.
   - qauto use:Univ_EPar', EPar.refl.
+  - qauto use:Bot_EPar', EPar.refl.
 Qed.
 
 Function tstar {n} (a : Tm n) :=
@@ -1537,6 +1568,7 @@ Function tstar {n} (a : Tm n) :=
   | TBind p a b => TBind p (tstar a) (tstar b)
   | Const k => Const k
   | Univ i => Univ i
+  | Bot => Bot
   end.
 
 Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a).
@@ -1555,6 +1587,7 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
+  - hauto lq:on inv:RPar.R ctrs:RPar.R.
 Qed.
 
 Function tstar' {n} (a : Tm n) :=
@@ -1569,6 +1602,7 @@ Function tstar' {n} (a : Tm n) :=
   | TBind p a b => TBind p (tstar' a) (tstar' b)
   | Const k => Const k
   | Univ i => Univ i
+  | Bot => Bot
   end.
 
 Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
@@ -1585,6 +1619,7 @@ Proof.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
 Qed.
 
 Lemma RPar_diamond n (c a1 b1 : Tm n) :
@@ -1651,7 +1686,9 @@ Inductive prov {n} : Tm n -> Tm n -> Prop :=
 | P_Var i :
   prov (VarTm i) (VarTm i)
 | P_Univ i :
-  prov (Univ i) (Univ i).
+  prov (Univ i) (Univ i)
+| P_Bot :
+  prov Bot Bot.
 
 Lemma ERed_EPar n (a b : Tm n) : ERed.R a b -> EPar.R a b.
 Proof.
@@ -1671,6 +1708,7 @@ Proof.
   - eauto using EReds.BindCong.
   - auto using rtc_refl.
   - auto using rtc_refl.
+  - auto using rtc_refl.
 Qed.
 
 Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b.
@@ -1723,6 +1761,7 @@ Proof.
   - hauto lq:on ctrs:prov inv:RPar.R.
   - hauto l:on ctrs:RPar.R inv:RPar.R.
   - hauto l:on ctrs:RPar.R inv:RPar.R.
+  - hauto l:on ctrs:RPar.R inv:RPar.R.
 Qed.
 
 
@@ -1777,6 +1816,7 @@ Proof.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
+  - hauto lq:on inv:ERed.R, prov ctrs:prov.
 Qed.
 
 Lemma prov_ereds n (u : Tm n) a b : prov u a -> rtc ERed.R a b -> prov u b.
@@ -1787,13 +1827,14 @@ Qed.
 Fixpoint extract {n} (a : Tm n) : Tm n :=
   match a with
   | TBind p A B => TBind p A B
-  | Abs a => subst_Tm (scons (Const TPi) VarTm) (extract a)
+  | Abs a => subst_Tm (scons Bot VarTm) (extract a)
   | App a b => extract a
   | Pair a b => extract a
   | Proj p a => extract a
   | Const k => Const k
   | VarTm i => VarTm i
   | Univ i => Univ i
+  | Bot => Bot
   end.
 
 Lemma ren_extract n m (a : Tm n) (ξ : fin n -> fin m) :
@@ -1810,6 +1851,7 @@ Proof.
   - hauto q:on.
   - sfirstorder.
   - sfirstorder.
+  - sfirstorder.
 Qed.
 
 Lemma ren_morphing n m (a : Tm n) (ρ : fin n -> Tm m) :
@@ -1828,7 +1870,7 @@ Proof.
 Qed.
 
 Lemma ren_subst_bot n (a : Tm (S n)) :
-  extract (subst_Tm (scons (Const TPi) VarTm) a) = subst_Tm (scons (Const TPi) VarTm) (extract a).
+  extract (subst_Tm (scons Bot VarTm) a) = subst_Tm (scons Bot VarTm) (extract a).
 Proof.
   apply ren_morphing. destruct i as [i|] => //=.
 Qed.
@@ -1839,6 +1881,7 @@ Definition prov_extract_spec {n} u (a : Tm n) :=
   | Univ i => extract a = Univ i
   | VarTm i => extract a = VarTm i
   | (Const i) => extract a = (Const i)
+  | Bot => extract a = Bot
   | _ => True
   end.
 
@@ -1851,24 +1894,28 @@ Proof.
   - move => h a ha ih.
     case : h ha ih => //=.
     + move => i ha ih.
-      move /(_ (Const TPi)) in ih.
+      move /(_ Bot) in ih.
       rewrite -ih.
       by rewrite ren_subst_bot.
     + move => p A B h ih.
-      move /(_ (Const TPi)) : ih => [A0][B0][h0][h1]h2.
+      move /(_ Bot) : ih => [A0][B0][h0][h1]h2.
       rewrite ren_subst_bot in h0.
       rewrite h0.
       eauto.
-    + move => p _ /(_ (Const TPi)).
+    + move => p _ /(_ Bot).
       by rewrite ren_subst_bot.
-    + move => i h /(_ (Const TPi)).
+    + move => i h /(_ Bot).
       by rewrite ren_subst_bot => ->.
+    + move /(_ Bot).
+      move => h /(_ Bot).
+      by rewrite ren_subst_bot.
   - hauto lq:on.
   - hauto lq:on.
   - hauto lq:on.
   - case => //=.
   - sfirstorder.
   - sfirstorder.
+  - sfirstorder.
 Qed.
 
 Definition union {A : Type} (R0 R1 : A -> A -> Prop) a b :=
@@ -2072,6 +2119,7 @@ Proof.
   - sfirstorder use:ERPars.BindCong.
   - sfirstorder.
   - sfirstorder.
+  - sfirstorder.
 Qed.
 
 Lemma Pars_ERPar n (a b : Tm n) : rtc Par.R a b -> rtc ERPar.R a b.
@@ -2371,18 +2419,19 @@ Fixpoint ne {n} (a : Tm n) :=
   | Proj _ a => ne a
   | Pair _ _ => false
   | Const _ => false
+  | Bot => true
   end
 with nf {n} (a : Tm n) :=
   match a with
   | VarTm i => true
   | TBind _ A B => nf A && nf B
-  | (Const TPi) => true
   | App a b => ne a && nf b
   | Abs a => nf a
   | Univ _ => true
   | Proj _ a => ne a
   | Pair a b => nf a && nf b
   | Const _ => true
+  | Bot => true
 end.
 
 Lemma ne_nf n a : @ne n a -> nf a.
@@ -2469,10 +2518,10 @@ Proof.
 Qed.
 
 Lemma ext_wn n (a : Tm n) :
-    wn (App a (Const TPi)) ->
+    wn (App a Bot) ->
     wn a.
 Proof.
-  move E : (App a (Const TPi)) => a0 [v [hr hv]].
+  move E : (App a (Bot)) => a0 [v [hr hv]].
   move : a E.
   move : hv.
   elim : a0 v / hr.
@@ -2483,9 +2532,9 @@ Proof.
     case : a0 hr0=>// => b0 b1.
     elim /RPar'.inv=>// _.
     + move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst.
-      have ? : b3 = (Const TPi) by hauto lq:on inv:RPar'.R. subst.
+      have ? : b3 = (Bot) by hauto lq:on inv:RPar'.R. subst.
       suff : wn (Abs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn.
-      have : wn (subst_Tm (scons (Const TPi) VarTm) a3) by sfirstorder.
+      have : wn (subst_Tm (scons (Bot) VarTm) a3) by sfirstorder.
       move => h. apply wn_abs.
       move : h. apply wn_antirenaming.
       hauto lq:on rew:off inv:option.

theories/logrel.v

@@ -1,5 +1,4 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red compile.
-Require Import fp_red.
 From Hammer Require Import Tactics.
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
@@ -295,9 +294,9 @@ Proof.
   - hauto lq:on ctrs:prov.
   - hauto lq:on rew:off ctrs:prov b:on.
   - hauto lq:on ctrs:prov.
-  - move => n.
+  - move => n k.
     have : @prov n Bot Bot by auto using P_Bot.
-    tauto.
+    eauto.
 Qed.
 
 Lemma ne_pars_inv n (a b : Tm n) :
@@ -311,23 +310,37 @@ Lemma ne_pars_extract  n (a b : Tm n) :
   ne a -> rtc Par.R a b -> (exists i, extract b = (VarTm i)) \/ extract b = Bot.
 Proof. hauto lq:on rew:off use:ne_pars_inv, prov_extract. Qed.
 
+Lemma const_pars_extract n k b :
+  rtc Par.R (Const k : Tm n) b -> extract b = Const k.
+Proof. hauto l:on use:pars_const_inv, prov_extract. Qed.
+
+Lemma compile_ne n (a : Tm n) :
+  ne a = ne (Compile.F a) /\ nf a = nf (Compile.F a).
+Proof.
+  elim : n / a => //=; sfirstorder b:on.
+Qed.
+
 Lemma join_bind_ne_contra n p (A : Tm n) B C :
   ne C ->
-  join (TBind p A B) C -> False.
+  Join.R (TBind p A B) C -> False.
 Proof.
-  move => hC [D [h0 h1]].
+  rewrite /Join.R. move => hC /=.
-  move /pars_pi_inv : h0 => [A0 [B0 [h2 [h3 h4]]]].
+  rewrite !pair_eq.
+  move => [[[D [h0 h1]] _] _].
+  have {}hC : ne (Compile.F C) by hauto lq:on use:compile_ne.
+  have {}hC : ne (Proj PL (Proj PL (Compile.F C))) by scongruence.
   have : (exists i, extract D = (VarTm i)) \/ extract D = Bot by eauto using ne_pars_extract.
+  have : extract D = Const p by eauto using const_pars_extract.
   sfirstorder.
 Qed.
 
 Lemma join_univ_ne_contra n i C :
   ne C ->
-  join (Univ i : Tm n) C -> False.
+  Join.R (Univ i : Tm n) C -> False.
 Proof.
   move => hC [D [h0 h1]].
   move /pars_univ_inv : h0 => ?.
-  have : (exists i, extract D = (VarTm i)) \/ extract D = Bot by eauto using ne_pars_extract.
+  have : (exists i, extract D = (VarTm i)) \/ exists k, extract D =(Const k)  by hauto q:on use:ne_pars_extract, compile_ne.
   sfirstorder.
 Qed.
 
@@ -336,7 +349,7 @@ Qed.
 Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ B ⟧ i ;; I ↘ PB ->
-  join A B ->
+  Join.R A B ->
   PA = PB.
 Proof.
   move => h. move : B PB. elim : A PA /h.