proposition: Lemma subterm_eq_var : forall u x, subterm_eq u (Var x) -> u = Var x.
proof: Proof. intros. unfold subterm_eq in H. destruct H as [C]. assert (C = Hole /\ u = Var x). apply var_eq_fill. exact H. destruct H0. exact H1. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)