proposition: Lemma if_cnf_tt : forall f, (if is_cnf_tt f then cnf_tt else f) = f.
proof: Proof. intros f. destruct (is_cnf_tt f) eqn:EQ. - apply is_cnf_tt_inv in EQ;auto. - reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid