proposition: Lemma equiv_AppR_elim s1 s2 T1 T2: AppR s1 T1 ≡ AppR s2 T2 -> isAtom s1 -> isAtom s2 -> T1 ≡₊ T2 /\ s1 = s2.
proof: Proof. intros; assert (isAtom (head (AppR s1 T1))); simplify; (eauto 2). intros; assert (isAtom (head (AppR s2 T2))); simplify; (eauto 2). revert T2 H H2 H3; induction T1 as [|a A IH]; intros [| b B]; cbn; intros. + intuition. destruct s1, s2; cbn in *; intuition; try Discriminate. all: Injection H; now subst. + destruct s1; cbn in *; try now intuition; Discriminate. + destruct s2; cbn in *; try now intuition; Discriminate. + Injection H. intuition; edestruct IH; (eauto 2). now rewrite H5, H. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)