proposition: Lemma eq_term_term_bool_ok : forall t1_t2 t1'_t2', if eq_term_term_bool t1_t2 t1'_t2' then t1_t2 = t1'_t2' else t1_t2 <> t1'_t2'.
proof: Proof. intros [t1 t2] [t1' t2']. simpl. generalize (M.eq_bool_ok t1 t1'). case (eq_bool t1 t1'). generalize (M.eq_bool_ok t2 t2'). case (eq_bool t2 t2'). intros;subst;reflexivity. intros t2_neq_t2' _ abs;elim t2_neq_t2';injection abs;intros;assumption. intros t1_neq_t1' abs;elim t1_neq_t1';injection abs;intros;assumption. Defined.
imports: Coq(List Bool) CoLoR(TransClosure)