proposition: Lemma fill_eq : forall t u c, fill c t = fill c u <-> t = u.
proof: Proof. split. induction c; simpl; intros. hyp. Funeqtac. rewrite Vcast_eq, Vapp_eq in H0. decomp H0. rewrite Vcons_eq in H1. intuition. intro. subst. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)