proposition: Lemma equiv_AppL_elim S1 S2 t1 t2: AppL S1 t1 ≡ AppL S2 t2 -> (forall s, s ∈ S1 -> isAtom (head s)) -> (forall s, s ∈ S2 -> isAtom (head s)) -> length S1 = length S2 -> S1 ≡₊ S2 /\ t1 ≡ t2.
proof: Proof. revert S2; induction S1 as [|s1 S1 IH]; intros [| s2 S2]; cbn; intros; try discriminate. + intuition. + apply equiv_app_elim in H as ?; rewrite ?AppR_head; (eauto 3). intuition; edestruct IH; (eauto 3). now rewrite H3, H4. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)