proposition: Lemma remove_unknown_prop : stable_atom_tree remove_unknown_func.
proof: Proof. intros [[l|] v [u|]|x y l u|v w|v w|f x|f x] pos ; try (case pos ; easy) ; simpl ; intros H. destruct l as [xl|xl|xl yl|xl yl|ol xl|ol xl yl|xl|xl|xl|xl|xl|xl|fl xl] ; try easy. destruct u as [xu|xu|xu yu|xu yu|ou xu|ou xu yu|xu|xu|xu|xu|xu|xu|fu xu] ; try easy. now destruct pos. destruct l as [l|l|l l'|l l'|o l|o l l'|l|l|l|l|l|l|f l] ; try easy. now destruct pos. destruct u as [u|u|u u'|u u'|o u|o u u'|u|u|u|u|u|u|f u] ; try easy. now destruct pos. destruct l as [l|l|l l'|l l'|o l|o l l'|l|l|l|l|l|l|f l] ; try easy. destruct u as [u|u|u u'|u u'|o u|o u u'|u|u|u|u|u|u|f u] ; try easy. now destruct pos. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library