proposition: Lemma eq_tt_bool_ok : forall t12 t12', match eq_tt_bool t12 t12' with true => t12 = t12' | false => t12 <> t12' end.
proof: Proof. unfold eq_tt_bool; intros [t1 t2] [t1' t2']; generalize (eq_bool_ok t1 t1'); case (eq_bool t1 t1'). intro t1_eq_t1'; generalize (eq_bool_ok t2 t2'); case (eq_bool t2 t2'). intro t2_eq_t2'; simpl; subst; reflexivity. intro t2_diff_t2'; simpl; intro H; apply t2_diff_t2'; injection H; intros; assumption. intro t1_diff_t1'; simpl; intro H; apply t1_diff_t1'; injection H; intros; assumption. Defined.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)