proposition: Lemma bsubterm_eq_ok : forall t u, bsubterm_eq t u = true <-> subterm_eq t u.
proof: Proof. intros t u. pattern u; apply term_ind_forall; clear u; simpl. intro. rewrite beq_term_ok. split; intro. subst. refl. apply subterm_eq_var in H. hyp. split; rewrite orb_eq, beq_term_ok; intros. destruct H0. subst. refl. rewrite (bVexists_ok_Vin (subterm_eq t)) in H0. 2:{ intros. pattern x. apply Vforall_in with (v:=v). apply H. hyp. } rewrite Vexists_eq in H0. decomp H0. apply subterm_eq_trans with x. hyp. apply subterm_strict. apply subterm_fun. hyp. destruct H0. destruct x. auto. right. rewrite (bVexists_ok_Vin (subterm_eq t)). 2:{ intros. pattern x0. apply Vforall_in with (v:=v). apply H. hyp. } rewrite Vexists_eq. exists (fill x t). split. simpl in H0. Funeqtac. rewrite H1, Vin_cast. apply Vin_app_cons. exists x. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)