(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export bg_types.
Require Export bg_tactics.

   Section bg_props. (* properties about generated types ********************)

      Lemma ex2_sym: (A:Set; P,Q:A->Prop)
                     (EX x | (P x) & (Q x)) -> (EX x | (Q x) & (P x)).
      Proof.
      Intros; XElim H; XDEAuto 2.
      Qed.

   End bg_props.