proposition: Lemma is_atom_app : forall e a b, is_atom e a -> is_atom e (App a b).
proof: Proof. intros e a b (n, lt_n, (l, eq_atom)). rewrite eq_atom. split with n; trivial. split with (b :: l); trivial. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia