1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1A/theory.ma".
19 axiom pc3_gen_appls_sort_abst:
20 \forall (c: C).(\forall (vs: TList).(\forall (w: T).(\forall (u: T).(\forall
21 (n: nat).((pc3 c (THeads (Flat Appl) vs (TSort n)) (THead (Bind Abst) w u))
25 axiom pc3_gen_appls_lref_abst:
26 \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
27 (CHead d (Bind Abst) v)) \to (\forall (vs: TList).(\forall (w: T).(\forall
28 (u: T).((pc3 c (THeads (Flat Appl) vs (TLRef i)) (THead (Bind Abst) w u)) \to
32 axiom pc3_gen_appls_lref_sort:
33 \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
34 (CHead d (Bind Abst) v)) \to (\forall (vs: TList).(\forall (ws:
35 TList).(\forall (n: nat).((pc3 c (THeads (Flat Appl) vs (TLRef i)) (THeads
36 (Flat Appl) ws (TSort n))) \to False))))))))