proposition: Lemma eval_is_close V x v (t: Term0 et V x): eval et v t ≡ close _ v t.
proof: Proof. Proof with auto; try reflexivity. pattern x, t. apply applications_rect; simpl... intro. cut (@equiv _ (structural_eq _) (app_tree (close _ v (Op et _ o))) (eval et v (Op et _ o)))... generalize (Op et V o). induction (et o); simpl... intros ? H ? E. apply IHo0. simpl. rewrite E. apply H... Qed.
imports: Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Classes.Morphisms MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.categories.varieties