proposition: Lemma atom_head_lifting (s: exp X) (sigma: fin -> exp X): (forall x, isAtom (head (sigma x))) -> isAtom (head s) -> isAtom (head (sigma • s)).
proof: Proof. induction s; cbn; intuition. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)