proposition: Lemma head_preserved s s': s > s' -> isLam (head s') -> isLam (head s).
proof: Proof. induction 1; cbn; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun