proposition: Lemma multiplication_lambdas M m p: normal M -> Grel m p M -> (exists M', M = (lambda lambda lambda M') /\ σ p m • M' = t 0 ::: (τ • M')).
proof: Proof. unfold Grel, Pair, Cons. cbn. intros Nu EQ. remember (fun m : nat => S (S m)) as delta. rename M into u. assert (normal (ren delta u)) as N' by (subst; eapply normal_ren; eauto). do 2 apply equiv_lam_elim in EQ. destruct u as [| | u' | ]; unfold funcomp; cbn in EQ. 4: eapply head_atom in N'; auto. 1, 2, 4: Injection EQ; Injection H; Discriminate. rewrite stepBeta in EQ; trivial. asimpl in EQ. rewrite stepBeta in EQ; trivial. asimpl in EQ. destruct u' as [[]| | u' | ]; cbn in EQ. 1 - 3: Injection EQ; Injection H; Discriminate. - do 2 (rewrite stepBeta in EQ; trivial; asimpl in EQ; cbn in EQ). destruct u' as [[|[]] | | u' | u1 u2 ]; cbn in EQ. 1 - 4: Injection EQ; unfold funcomp in *; Discriminate. + exists u'. intuition idtac. do 2 (rewrite stepBeta in EQ; trivial; asimpl in EQ; cbn in EQ). repeat eapply normal_lam_elim in Nu. eapply equiv_unique_normal_forms; [trivial | trivial |..]. subst delta; exact EQ. 2: eapply normal_app_intro; cbn; intuition idtac. 2: repeat eapply normal_app_intro; auto. all: eapply normal_subst; try eassumption. all: intros [|[|[]]]; cbn; auto 2. all: unfold funcomp, Nil; (repeat eapply normal_app_intro); auto. destruct n; simplify; auto. + exfalso. repeat eapply normal_lam_elim in Nu. eapply head_atom in Nu as H'; [|auto]. eapply atom_head_lifting with (sigma := A .: g (g (enc p A) (enc m B)) (id Nil) .: delta >> var) in H' as H4. 2: intros [|[]]; cbn; auto. cbn in H4. Injection EQ. Injection H. destruct u1 as [[|[]]|[]| |]; cbn in H1; try Injection EQ; try Discriminate. - eapply normal_lam_elim in Nu. eapply head_atom in Nu; auto. eapply atom_head_lifting with (sigma := g (g (enc p A) (enc m B)) Nil .: delta >> var) in Nu; cbn in Nu. 2: intros []; cbn; trivial. Injection EQ. Injection H. Discriminate. Qed.
imports: List Lia Program.Program Undecidability.HOU(std.std axioms) RelationClasses Morphisms Init.Wf Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.goldfarb.encoding) FinFun Coq.Arith.Wf_nat