proposition: Lemma wf_term : forall (t : term) c, t = fill c t -> c = Hole.
proof: Proof. intros. destruct c. refl. assert (size (fill (Cont e t0 c t1) t) > size t). simpl fill. rewrite size_fun, size_terms_cast, size_terms_app. simpl. ded (size_fill t c). lia. rewrite <- H in H0. lia. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)