yiyunliu/pair-eta
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Need to change the ifproj rules

Browse source
This commit is contained in:
Yiyun Liu 2025-01-12 17:35:34 -05:00
parent bc848e91ea
commit 76050bc511
1 changed files with 253 additions and 182 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

435
theories/fp_red.v
View file

@ -376,36 +376,34 @@ Module RPar.
Inductive R {n} : Tm n -> Tm n -> Prop := Inductive R {n} : Tm n -> Tm n -> Prop :=
(***************** Beta ***********************) (***************** Beta ***********************)
| AppAbs a0 a1 b0 b1 : | AppAbs a0 a1 b0 b1 :
R a0 a1 -> R a0 (Abs a1) ->
R b0 b1 ->
R (App (Abs a0) b0) (subst_Tm (scons b1 VarTm) a1)
| AppPair a0 a1 b0 b1 c0 c1:
R a0 a1 ->
R b0 b1 -> R b0 b1 ->
R (App a0 b0) (subst_Tm (scons b1 VarTm) a1)
| AppPair a a0 b0 c0 c1:
R a (Pair a0 b0) ->
R c0 c1 -> R c0 c1 ->
R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) R (App a c0) (Pair (App a0 c1) (App b0 c1))
| ProjAbs p a0 a1 : | ProjAbs p a0 a1 :
R a0 a1 -> R a0 (Abs a1) ->
R (Proj p (Abs a0)) (Abs (Proj p a1)) R (Proj p a0) (Abs (Proj p a1))
| ProjPair p a0 a1 b0 b1 : | ProjPair p a b c :
R a0 a1 -> R a (Pair b c) ->
R b0 b1 -> R (Proj p a) (if p is PL then b else c)
R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) | IfAbs a0 a1 b0 b1 c0 c1 :
| IfAbs (a0 a1 : Tm (S n)) b0 b1 c0 c1 : R a0 (Abs a1) ->
R a0 a1 ->
R b0 b1 -> R b0 b1 ->
R c0 c1 -> R c0 c1 ->
R (If (Abs a0) b0 c0) (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) R (If a0 b0 c0) (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1)))
| IfPair a0 a1 b0 b1 c0 c1 d0 d1 : | IfPair a a0 a1 c0 c1 d0 d1 :
R a0 a1 -> R a (Pair a0 a1) ->
R b0 b1 ->
R c0 c1 -> R c0 c1 ->
R d0 d1 -> R d0 d1 ->
R (If (Pair a0 b0) c0 d0) (Pair (If a1 c1 d1) (If b1 c1 d1)) R (If a c0 d0) (Pair (If a0 c1 d1) (If a1 c1 d1))
| IfBool a b0 b1 c0 c1 : | IfBool a v b0 b1 c0 c1 :
R a (BVal v) ->
R b0 b1 -> R b0 b1 ->
R c0 c1 -> R c0 c1 ->
R (If (BVal a) b0 c0) (if a then b1 else c1) R (If a b0 c0) (if v then b1 else c1)
(*************** Congruence ********************) (*************** Congruence ********************)
@ -460,41 +458,42 @@ Module RPar.
induction a; hauto lq:on ctrs:R. induction a; hauto lq:on ctrs:R.
Qed. Qed.
Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) : Lemma AppAbs' n (a0 : Tm n) a1 b0 b1 u :
t = subst_Tm (scons b1 VarTm) a1 -> u = (subst_Tm (scons b1 VarTm) a1) ->
R a0 a1 -> R a0 (Abs a1) ->
R b0 b1 -> R b0 b1 ->
R (App (Abs a0) b0) t. R (App a0 b0) u.
Proof. move => ->. apply AppAbs. Qed. Proof. move => ->. apply AppAbs. Qed.
Lemma ProjPair' n p (a0 a1 b0 b1 : Tm n) t : Lemma ProjPair' n p a b c u :
t = (if p is PL then a1 else b1) -> u = (if p is PL then b else c) ->
R a0 a1 -> R a (Pair b c : Tm n) ->
R b0 b1 -> R (Proj p a) u.
R (Proj p (Pair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed.
Proof. move => > ->. apply ProjPair. Qed.
Lemma IfBool' n a b0 b1 c0 c1 u : Lemma IfBool' n a v b0 b1 c0 c1 u :
u = (if a then (b1 : Tm n) else c1) -> u = (if v then b1 else c1) ->
R a (BVal v : Tm n) ->
R b0 b1 -> R b0 b1 ->
R c0 c1 -> R c0 c1 ->
R (If (BVal a) b0 c0) u. R (If a b0 c0) u.
Proof. move => ->. apply IfBool. Qed. Proof. move => ->. apply IfBool. Qed.
Lemma IfAbs' n a0 (a1 : Tm (S n)) (b0 b1 c0 c1 : Tm n) u :
Lemma IfAbs' n (a0 a1 : Tm (S n)) (b0 b1 c0 c1 : Tm n) u :
u = (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) -> u = (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) ->
@R (S n) a0 a1 -> @R n a0 (Abs a1) ->
R b0 b1 -> R b0 b1 ->
R c0 c1 -> R c0 c1 ->
R (If (Abs a0) b0 c0) u. R (If a0 b0 c0) u.
Proof. move => ->. apply IfAbs. Qed. Proof. move => ->. apply IfAbs. Qed.
Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) :
R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). R a b -> R (ren_Tm ξ a) (ren_Tm ξ b).
Proof. Proof.
move => h. move : m ξ. move => h. move : m ξ.
elim : n a b /h; try solve [(move => *; apply : AppAbs'; eauto; by asimpl) | (move => *; apply : IfAbs'; eauto; by asimpl)]. elim : n a b /h => //=; try solve [(move => *; apply : AppAbs'; eauto; rewrite -/ren_Tm;by asimpl) |
(move => *; apply : IfBool'; eauto; rewrite -/ren_Tm; hauto lq:on) |
(move => *; apply : IfAbs'; eauto; rewrite -/ren_Tm; by asimpl)].
all : try qauto ctrs:R use:ProjPair', IfBool'. all : try qauto ctrs:R use:ProjPair', IfBool'.
Qed. Qed.
@ -520,17 +519,18 @@ Module RPar.
Proof. Proof.
move => + h. move : m ρ0 ρ1. move => + h. move : m ρ0 ρ1.
elim : n a b /h. elim : n a b /h.
- move => *. - move => /= *.
apply : AppAbs'; eauto using morphing_up. apply : AppAbs'; eauto using morphing_up.
by asimpl. by asimpl.
- hauto lq:on ctrs:R. - hauto lq:on ctrs:R.
- hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up.
- hauto lq:on ctrs:R use:ProjPair' use:morphing_up. - hauto lq:on ctrs:R use:ProjPair' use:morphing_up.
- move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=. - move => /= *.
apply : IfAbs'; eauto using morphing_up. apply : IfAbs'; eauto using morphing_up.
by asimpl. by asimpl.
- hauto lq:on ctrs:R. - hauto lq:on ctrs:R.
- hauto lq:on ctrs:R use:IfBool' use:morphing_up. - move => n a v b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=.
eapply IfBool' with (v := v); qauto l:on.
- hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up.
- hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up.
- hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up.
@ -585,145 +585,145 @@ Module RPar.
Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
(forall i, var_or_bot (ρ i)) -> (forall i, var_or_bot (ρ i)) ->
R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b. R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b.
Proof. (* Proof. *)
move E : (subst_Tm ρ a) => u hρ h. (* move E : (subst_Tm ρ a) => u hρ h. *)
move : n ρ hρ a E. elim : m u b/h. (* move : n ρ hρ a E. elim : m u b/h. *)
- move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; (* - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *)
first by antiimp. (* first by antiimp. *)
move => c c0 [+ ?]. subst. (* move => c c0 [+ ?]. subst. *)
case : c => //=; first by antiimp. (* case : c => //=; first by antiimp. *)
move => c [?]. subst. (* move => c [?]. subst. *)
spec_refl. (* spec_refl. *)
have /var_or_bot_up hρ' := hρ. (* have /var_or_bot_up hρ' := hρ. *)
move : iha hρ' => /[apply] iha. (* move : iha hρ' => /[apply] iha. *)
move : ihb hρ => /[apply] ihb. (* move : ihb hρ => /[apply] ihb. *)
spec_refl. (* spec_refl. *)
move : iha => [c1][ih0]?. subst. (* move : iha => [c1][ih0]?. subst. *)
move : ihb => [c2][ih1]?. subst. (* move : ihb => [c2][ih1]?. subst. *)
eexists. split. (* eexists. split. *)
apply AppAbs; eauto. (* apply AppAbs; eauto. *)
by asimpl. (* by asimpl. *)
- move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; (* - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; *)
first by antiimp. (* first by antiimp. *)
move => []//=; first by antiimp. (* move => []//=; first by antiimp. *)
move => t t0 t1 [*]. subst. (* move => t t0 t1 [*]. subst. *)
have {}/iha := hρ => iha. (* have {}/iha := hρ => iha. *)
have {}/ihb := hρ => ihb. (* have {}/ihb := hρ => ihb. *)
have {}/ihc := hρ => ihc. (* have {}/ihc := hρ => ihc. *)
spec_refl. (* spec_refl. *)
move : iha => [? [*]]. (* move : iha => [? [*]]. *)
move : ihb => [? [*]]. (* move : ihb => [? [*]]. *)
move : ihc => [? [*]]. (* move : ihc => [? [*]]. *)
eexists. split. (* eexists. split. *)
apply AppPair; hauto. subst. (* apply AppPair; hauto. subst. *)
by asimpl. (* by asimpl. *)
- move => n p a0 a1 ha iha m ρ hρ []//=; (* - move => n p a0 a1 ha iha m ρ hρ []//=; *)
first by antiimp. (* first by antiimp. *)
move => p0 []//= t [*]; first by antiimp. subst. (* move => p0 []//= t [*]; first by antiimp. subst. *)
have /var_or_bot_up {}/iha := hρ => iha. (* have /var_or_bot_up {}/iha := hρ => iha. *)
spec_refl. move : iha => [b0 [? ?]]. subst. (* spec_refl. move : iha => [b0 [? ?]]. subst. *)
eexists. split. apply ProjAbs; eauto. by asimpl. (* eexists. split. apply ProjAbs; eauto. by asimpl. *)
- move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; (* - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *)
first by antiimp. (* first by antiimp. *)
move => p0 []//=; first by antiimp. move => t t0[*]. (* move => p0 []//=; first by antiimp. move => t t0[*]. *)
subst. (* subst. *)
have {}/iha := (hρ) => iha. (* have {}/iha := (hρ) => iha. *)
have {}/ihb := (hρ) => ihb. (* have {}/ihb := (hρ) => ihb. *)
spec_refl. (* spec_refl. *)
move : iha => [b0 [? ?]]. (* move : iha => [b0 [? ?]]. *)
move : ihb => [c0 [? ?]]. subst. (* move : ihb => [c0 [? ?]]. subst. *)
eexists. split. by eauto using ProjPair. (* eexists. split. by eauto using ProjPair. *)
hauto q:on. (* hauto q:on. *)
- move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp. (* - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp. *)
move => + b2 c2 [+ *]. subst. case => //=; first by antiimp. (* move => + b2 c2 [+ *]. subst. case => //=; first by antiimp. *)
move => a [*]. subst. (* move => a [*]. subst. *)
have /var_or_bot_up hρ' := hρ. (* have /var_or_bot_up hρ' := hρ. *)
move : iha hρ' => /[apply] iha. (* move : iha hρ' => /[apply] iha. *)
move : ihb (hρ) => /[apply] ihb. (* move : ihb (hρ) => /[apply] ihb. *)
move : ihc hρ => /[apply] ihc. (* move : ihc hρ => /[apply] ihc. *)
spec_refl. (* spec_refl. *)
move : iha => [a0 [ha0 ?]]. subst. (* move : iha => [a0 [ha0 ?]]. subst. *)
move : ihb => [b0 [hb0 ?]]. subst. (* move : ihb => [b0 [hb0 ?]]. subst. *)
move : ihc => [c0 [hc0 ?]]. subst. (* move : ihc => [c0 [hc0 ?]]. subst. *)
exists (Abs (If a0 (ren_Tm shift b0) (ren_Tm shift c0))). split. (* exists (Abs (If a0 (ren_Tm shift b0) (ren_Tm shift c0))). split. *)
hauto lq:on ctrs:R. (* hauto lq:on ctrs:R. *)
by asimpl. (* by asimpl. *)
- move => n a0 a1 b0 b1 c0 c1 d0 d1 ha iha hb ihb hc ihc hd ihd m ρ hρ []//=; first by antiimp. (* - move => n a0 a1 b0 b1 c0 c1 d0 d1 ha iha hb ihb hc ihc hd ihd m ρ hρ []//=; first by antiimp. *)
move => a2 b2 c2 [+ *]. subst. case : a2 => //=; first by antiimp. (* move => a2 b2 c2 [+ *]. subst. case : a2 => //=; first by antiimp. *)
move => a3 b3 [*]. subst. (* move => a3 b3 [*]. subst. *)
have {}/iha := (hρ) => iha. (* have {}/iha := (hρ) => iha. *)
have {}/ihb := (hρ) => ihb. (* have {}/ihb := (hρ) => ihb. *)
have {}/ihc := (hρ) => ihc. (* have {}/ihc := (hρ) => ihc. *)
spec_refl. (* spec_refl. *)
hauto lq:on ctrs:R. (* hauto lq:on ctrs:R. *)
- move => n a b0 b1 c0 c1 hb ihb hc ihc m ρ hρ []//=; first by antiimp. (* - move => n a b0 b1 c0 c1 hb ihb hc ihc m ρ hρ []//=; first by antiimp. *)
move => t t0 t1 [h *]. subst. (* move => t t0 t1 [h *]. subst. *)
case : t h => //=; first by antiimp. (* case : t h => //=; first by antiimp. *)
move => b [*]. subst. (* move => b [*]. subst. *)
have {}/ihb := (hρ) => ihb. (* have {}/ihb := (hρ) => ihb. *)
have {}/ihc := (hρ) => ihc. (* have {}/ihc := (hρ) => ihc. *)
spec_refl. (* spec_refl. *)
hauto q:on use:IfBool. (* hauto q:on use:IfBool. *)
- move => n i m ρ hρ []//=. (* - move => n i m ρ hρ []//=. *)
hauto l:on. (* hauto l:on. *)
- move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. (* - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. *)
move => t [*]. subst. (* move => t [*]. subst. *)
have /var_or_bot_up {}/iha := hρ => iha. (* have /var_or_bot_up {}/iha := hρ => iha. *)
spec_refl. (* spec_refl. *)
move :iha => [b0 [? ?]]. subst. (* move :iha => [b0 [? ?]]. subst. *)
eexists. split. by apply AbsCong; eauto. (* eexists. split. by apply AbsCong; eauto. *)
by asimpl. (* by asimpl. *)
- move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; (* - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *)
first by antiimp. (* first by antiimp. *)
move => t t0 [*]. subst. (* move => t t0 [*]. subst. *)
have {}/iha := (hρ) => iha. (* have {}/iha := (hρ) => iha. *)
have {}/ihb := (hρ) => ihb. (* have {}/ihb := (hρ) => ihb. *)
spec_refl. (* spec_refl. *)
move : iha => [b0 [? ?]]. subst. (* move : iha => [b0 [? ?]]. subst. *)
move : ihb => [c0 [? ?]]. subst. (* move : ihb => [c0 [? ?]]. subst. *)
eexists. split. by apply AppCong; eauto. (* eexists. split. by apply AppCong; eauto. *)
done. (* done. *)
- move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; (* - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *)
first by antiimp. (* first by antiimp. *)
move => t t0[*]. subst. (* move => t t0[*]. subst. *)
have {}/iha := (hρ) => iha. (* have {}/iha := (hρ) => iha. *)
have {}/ihb := (hρ) => ihb. (* have {}/ihb := (hρ) => ihb. *)
spec_refl. (* spec_refl. *)
move : iha => [b0 [? ?]]. subst. (* move : iha => [b0 [? ?]]. subst. *)
move : ihb => [c0 [? ?]]. subst. (* move : ihb => [c0 [? ?]]. subst. *)
eexists. split. by apply PairCong; eauto. (* eexists. split. by apply PairCong; eauto. *)
by asimpl. (* by asimpl. *)
- move => n p a0 a1 ha iha m ρ hρ []//=; (* - move => n p a0 a1 ha iha m ρ hρ []//=; *)
first by antiimp. (* first by antiimp. *)
move => p0 t [*]. subst. (* move => p0 t [*]. subst. *)
have {}/iha := (hρ) => iha. (* have {}/iha := (hρ) => iha. *)
spec_refl. (* spec_refl. *)
move : iha => [b0 [? ?]]. subst. (* move : iha => [b0 [? ?]]. subst. *)
eexists. split. apply ProjCong; eauto. reflexivity. (* eexists. split. apply ProjCong; eauto. reflexivity. *)
- move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=; (* - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=; *)
first by antiimp. (* first by antiimp. *)
move => ? t t0 [*]. subst. (* move => ? t t0 [*]. subst. *)
have {}/iha := (hρ) => iha. (* have {}/iha := (hρ) => iha. *)
have /var_or_bot_up {}/ihB := (hρ) => ihB. (* have /var_or_bot_up {}/ihB := (hρ) => ihB. *)
spec_refl. (* spec_refl. *)
move : iha => [b0 [? ?]]. (* move : iha => [b0 [? ?]]. *)
move : ihB => [c0 [? ?]]. subst. (* move : ihB => [c0 [? ?]]. subst. *)
eexists. split. by apply BindCong; eauto. (* eexists. split. by apply BindCong; eauto. *)
by asimpl. (* by asimpl. *)
- hauto q:on ctrs:R inv:Tm. (* - hauto q:on ctrs:R inv:Tm. *)
- move => n i n0 ρ hρ []//=; first by antiimp. (* - move => n i n0 ρ hρ []//=; first by antiimp. *)
hauto l:on. (* hauto l:on. *)
- move => n m ρ hρ []//=; first by antiimp. (* - move => n m ρ hρ []//=; first by antiimp. *)
hauto lq:on ctrs:R. (* hauto lq:on ctrs:R. *)
- move => n b m ρ hρ []//; first by antiimp. (* - move => n b m ρ hρ []//; first by antiimp. *)
hauto lq:on ctrs:R. (* hauto lq:on ctrs:R. *)
- move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp. (* - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp. *)
move => t t0 t1 [*]. subst. (* move => t t0 t1 [*]. subst. *)
have {}/iha := (hρ) => iha. (* have {}/iha := (hρ) => iha. *)
have {}/ihb := (hρ) => ihb. (* have {}/ihb := (hρ) => ihb. *)
have {}/ihc := (hρ) => ihc. (* have {}/ihc := (hρ) => ihc. *)
spec_refl. (* spec_refl. *)
hauto lq:on ctrs:R. (* hauto lq:on ctrs:R. *)
Admitted. Admitted.
Function tstar {n} (a : Tm n) := Function tstar {n} (a : Tm n) :=
@ -761,7 +761,78 @@ Module RPar.
apply tstar_ind => {n a}. apply tstar_ind => {n a}.
- 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.
- hauto lq:on use:RPar.cong, RPar.refl ctrs:RPar.R inv:RPar.R. - move => n a a0 b ? ih a1 eq ih2 b0. subst.
elim /inv => //= _.
+ move => a2 a3 b1 b2 h0 h1 [*]. subst.
apply cong; eauto.
apply ih in h0.
elim /inv : h0 => //=.
scongruence.
+ move => a2 a3 b1 c0 c1 h0 h1 [*]. subst.
move /ih : h0.
elim /inv => //=. scongruence.
+ hauto l:on use:AppAbs.
- move => n a a0 b ? ih a1 c e ih' h2 b0.
elim /inv => //= _.
+ move => a2 a3 b1 b2 ha hb [*]. subst.
have {}/ih := ha.
elim /inv => //=. scongruence.
+ move => a2 b3 b1 c0 c1 + + [*]. subst.
move /ih. elim/inv=>//=. move => ? a2 a3 b0 b2 ha hb [*]. subst.
apply PairCong; eauto;
apply AppCong; eauto; scongruence.
+ hauto l:on use:AppPair.
- move => n a a0 b ? ih c ? hc iha ihb. subst.
move => b0. elim /inv => //=.
+ qblast.
+ qblast.
+ hauto lq:on ctrs:R.
- hauto lq:on ctrs:R inv:R.
- move => n a p a0 ? ih a1 b h ?. subst.
move => b0. elim /inv => //= _.
+ sauto.
+ sauto.
+ move => p a2 a3 h0 [*]. subst.
have {}/ih := h0.
rewrite h. sfirstorder use:ProjPair'.
- move => n a p a0 ? ih a1 b ih2 p0 ?. subst.
case : p0 => //= _ b0.
elim /inv=>//=.
+ sauto.
+ sauto.
+ move => h p a2 a3 h0 [*]. subst.
have {}/ih := h0.
rewrite ih2. sfirstorder use:ProjPair'.
- sauto use:ProjAbs.
- move => n a p a0 ? ih ? ? h. subst.
move => h0 b.
elim /inv => //=.
+ sauto use:ProjAbs.
+ scrush use:ProjAbs.
+ sauto lq:on use:ProjAbs.
- hauto lq:on ctrs:R inv:R.
- hauto lq:on ctrs:R inv:R.
- hauto lq:on ctrs:R inv:R.
- hauto lq:on ctrs:R inv:R.
- hauto lq:on ctrs:R inv:R.
- move => n a a0 b c ? ih v eq ? hh. subst.
move => b0. elim /inv => //= _.
+ sauto q:on.
+ sauto q:on.
+ sauto.
+ move => a1 a2 b1 b2 c0 c1 ha hb hc [*]. subst.
apply ih in ha. apply hh in hb.
apply : IfBool'; eauto; cycle 1.
hauto q:on.
sfirstorder use:refl.
sfirstorder.
+ move => a1 a2 b1 b2 c0 c1 d0 d1 ha hb hc hd [*]. subst.
have {}/ih : R (App a1 b1) (App a2 b2) by eauto using AppCong.
rewrite eq.
elim /inv => //= _.
move => a0 a3 b0 b3 ha0 hb0 [*]. subst.
- hauto lq:on rew:off ctrs:RPar.R inv:RPar.R. - hauto lq:on rew:off ctrs:RPar.R inv:RPar.R.
- hauto lq:on rew:off inv:RPar.R ctrs:RPar.R. - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R.
- hauto lq:on rew:off inv:RPar.R ctrs:RPar.R. - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R.