proposition: Lemma or_is_X_inv : forall (k: kind) (f1 f2 : TFormula TX AF k), or_is_X f1 f2 = true -> exists k1, is_X f1 = Some k1 \/ is_X f2 = Some k1.
proof: Proof. unfold or_is_X. intros k f1 f2. is_X t; is_X t0. - exists t ; intuition. - exists t ; intuition. - exists t0 ; intuition. - congruence. Qed.
imports: List Refl Bool Relation_Definitions Setoid