proposition: Lemma bsubterm_ok : forall t u, bsubterm t u = true <-> subterm t u.
proof: Proof. destruct u; simpl. intuition. destruct H. destruct H. destruct x. cong. simpl in H0. discr. rewrite (bVexists_ok (subterm_eq t)), Vexists_eq. split; intro. decomp H. apply subterm_trans_eq1 with x. hyp. apply subterm_fun. hyp. apply subterm_fun_elim in H. hyp. apply bsubterm_eq_ok. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)