proposition: Lemma eq_bool_ok : forall n1 n2, if eq_bool n1 n2 then n1=n2 else n1<>n2.
proof: Proof. induction n1 as [|n1];intros [|n2];simpl in *. exact (eq_refl _). intro abs;discriminate abs. intro abs;discriminate abs. generalize (IHn1 n2). case (eq_bool n1 n2). intro Heq;f_equal;assumption. intros Hneq abs;elim Hneq;injection abs;intro H;exact H. Defined.
imports: Coq(List Bool) CoLoR(TransClosure)