proposition: Lemma var_eq_fill : forall x c t, Var x = fill c t -> c = Hole /\ t = Var x.
proof: Proof. intros. destruct c; simpl in H. auto. discr. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)