proposition: Lemma fun_eq_fill : forall f ts c u, Fun f ts = fill c u -> c = Hole \/ exists i, exists j, exists H : i + S j = arity f, exists ti, exists d, exists tj, c = Cont H ti d tj.
proof: Proof. intros. destruct c. auto. right. simpl in H. injection H. intros. subst f0. exists i. exists j. exists e. exists t. exists c. exists t0. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)