proposition: Lemma eq_bool_ok : forall a1 a2, match eq_bool a1 a2 with true => a1 = a2 | false => ~ a1 = a2 end.
proof: Proof. intros a1 a2. unfold eq_bool. case_beq_symb Sig a1 a2. refl. rewrite <- (beq_ko (@beq_symb_ok Sig)). hyp. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil)