helm/software/matita/tests/subsumption.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14 include "logic/equality.ma".
  15
  16 ntheorem foo :
  17   ∀U : Type.
  18   ∀a : U.
  19  ∀b : U.
  20   ∀f : U → U → U.
  21   ∀g : U → U → U.
  22   ∀H : ∀x.g x a = g a x.
  23   ∃y,z. f (g y b) y = f (g z a) a.
  24 #U. #a. #b. #f. #g. #H.
  25 napply (ex_intro ????);
  26 ##[ ##2: napply (ex_intro ????);
  27          ##[ ##2: nauto by H. ##| ##skip ##] ##| ##skip ##] nqed.
  28
  29 ntheorem foo1 :
  30   ∀U : Type.
  31   ∀a : U.
  32  ∀b : U.
  33   ∀f : U → U → U.
  34   ∀g : U → U → U.
  35   ∀H : ∀x.g x a = g a x.
  36   ∃y,z. f y (g y b) = f a (g z a).
  37 #U. #a. #b. #f. #g. #H.
  38 napply (ex_intro ????);
  39 ##[ ##2: napply (ex_intro ????);
  40          ##[ ##2: nauto by H. ##| ##skip ##] ##| ##skip ##] nqed.
  41
  42 ntheorem foo2 :
  43   ∀U : Type.
  44   ∀a : U.
  45  ∀b : U.
  46   ∀f : U → U → U.
  47   ∀g : U → U → U.
  48   ∀H : ∀x.g x a = g a x.
  49   ∃y,z. f (g z a) (g y b) = f (g y b) (g z a).
  50 #U. #a. #b. #f. #g. #H.
  51 napply (ex_intro ????);
  52 ##[ ##2: napply (ex_intro ????);
  53          ##[ ##2: nauto by H. ##| ##skip ##] ##| ##skip ##] nqed.
  54