proposition: Lemma is_bool_inv : forall {TX : kind -> Type} {AF: Type} (k: kind) (f : TFormula TX AF k) res, is_bool f = Some res -> f = if res then TT _ else FF _.
proof: Proof. intros TX AF k f res H. destruct f ; inversion H; reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid