proposition: Lemma fun_aeq_r : forall f v, v ~~ Fun f -> v = Fun f.
proof: Proof. intros x v h. sym. apply fun_aeq_l. sym. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)