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