proposition: Lemma cont_fun1 : forall f t, cont (Fun1 f t) = Cont1 f (cont t).
proof: Proof. intros. unfold Fun1, cont. fold cont. rewrite Vmap_first_cast. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)