proposition: Lemma fill_cont1 : forall f c t, fill (Cont1 f c) t = Fun1 f (fill c t).
proof: Proof. intros. unfold Cont1. unfold fill. fold (fill c t). simpl Vapp. unfold Fun1. apply args_eq. apply Vcast_pi. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)