proposition: Lemma fun_aeq_l : forall f v, Fun f ~~ v -> Fun f = v.
proof: Proof. intro f. cut (forall u v, u ~~ v -> (u = Fun f \/ v = Fun f) -> u = v). fo. induction 1; intro h; try (destruct h; discr). refl. fo. trans v. apply IHaeq1. destruct h as [h|h]. auto. subst. right. fo. apply IHaeq2. destruct h as [h|h]. subst. left. fo. auto. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)