proposition: Theorem arrow_unique: ∀ y, the_arrow = y.
proof: Proof. Proof with auto; try intuition. intros [x h] b a. simpl in *. pattern b, a. apply applications_rect... pose proof (@preserves et ClosedTerm0 other _ _ _ _ x h o). change (Preservation et ClosedTerm0 other x (app_tree (Op _ _ o)) (@eval_in_other _ (Op _ _ o))) in H. revert H. generalize (Op _ False o). induction (et o); simpl... apply IHo0. simpl in *. assert (app_tree (App _ _ o0 t t0 v) = app_tree (App _ _ o0 t t0 v)). apply app_tree_proper... apply (@Preservation_proper et ClosedTerm0 other _ _ x _ _ _ o0 (app_tree (App _ _ o0 t t0 v)) (app_tree (App _ _ o0 t t0 v)) H1 (eval_in_other t0 (eval_in_other v)) (eval_in_other t0 (x t v)))... pose proof (@prep_proper _ t0 t0 (reflexivity _))... 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