proposition: Lemma AppR_head s T: head (AppR s T) = head s.
proof: Proof. induction T in s |-*; cbn ; (eauto 1); now rewrite IHA. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)