module T = CicUtil
type status = {
- sorts : (Cic.id, Cic2acic.sort_kind) Hashtbl.t;
+ sorts : (C.id, Cic2acic.sort_kind) Hashtbl.t;
types : (C.id, A.anntypes) Hashtbl.t;
prefix: string;
max_depth: int option;
let cic = D.deannotate_term
let split2_last l1 l2 =
+try
let n = pred (List.length l1) in
let before1, after1 = P.list_split n l1 in
let before2, after2 = P.list_split n l2 in
before1, before2, List.hd after1, List.hd after2
+with Invalid_argument _ -> failwith "A2P.split2_last"
let string_of_head = function
| C.ASort _ -> "sort"
{st with entries = entry :: st.entries; intros = intro :: st.intros}
let test_depth st =
+try
let msg = Printf.sprintf "Depth %u: " st.depth in
match st.max_depth with
| None -> true, ""
| Some d ->
if st.depth < d then true, msg else false, "DEPTH EXCEDED"
+with Invalid_argument _ -> failwith "A2P.test_depth"
let get_itype st v =
+try
let id = T.id_of_annterm v in
try Some ((Hashtbl.find st.types id).A.annsynthesized)
with Not_found -> None
+with Invalid_argument _ -> failwith "A2P.get_itype"
(* proof construction *******************************************************)
let unused_premise = "UNUSED"
-let get_intro name t = match name with
+let get_intro name t =
+try
+match name with
| C.Anonymous -> unused_premise
| C.Name s ->
if DTI.does_not_occur 1 (cic t) then unused_premise else s
+with Invalid_argument _ -> failwith "A2P.get_intro"
let mk_intros st script =
+try
if st.intros = [] then script else
let count = List.length st.intros in
P.Intros (Some count, List.rev st.intros, "") :: script
+with Invalid_argument _ -> failwith "A2P.mk_intros"
let is_rewrite_right = function
| C.AConst (_, uri, []) ->
let mk_premise = function
| C.ARel (_, _, _, binder) -> binder
- | _ -> assert false
+ | C.AVar (_, uri, _)
+ | C.AConst (_, uri, _) -> UM.name_of_uri uri
+ | C.ASort (_, sort) -> assert false
+ | C.AMutInd (_, uri, tno, _) -> assert false
+ | C.AMutConstruct (_, uri, tno, cno, _) -> assert false
+ | _ -> assert false
let rec mk_fwd_proof st dtext name = function
| C.AAppl (_, hd :: tl) as v ->
| C.ALetIn (_, name, v, t) as what ->
let proceed, dtext = test_depth st in
let script = if proceed then
+ let entry = Some (name, C.Def (cic v, None)) in
let intro = get_intro name t in
- let q = mk_proof (next st) t in
+ let q = mk_proof (next (add st entry intro)) t in
List.rev_append (mk_fwd_proof st dtext intro v) q
else
[P.Apply (what, dtext)]
mk_intros st script
and mk_bkd_proofs st synth classes ts =
+try
let _, dtext = test_depth st in
let aux inv v =
if L.overlaps synth inv then None else
if L.S.is_empty inv then Some (mk_proof st v) else
Some [P.Apply (v, dtext ^ "dependent")]
in
+ let l1, l2 = List.length classes, List.length ts in
+ if l1 > l2 then failwith "partial application" else
+ if l1 < l2 then failwith "too many arguments" else
P.list_map2_filter aux classes ts
+with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
(* object costruction *******************************************************)
+let is_theorem pars =
+ List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars ||
+ List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
+
let mk_obj st = function
- | C.AConstant (_, _, s, Some v, t, [], _) ->
+ | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
let ast = mk_proof st v in
let count = P.count_steps 0 ast in
let text = Printf.sprintf "tactics: %u" count in
P.Theorem (s, t, text) :: ast @ [P.Qed ""]
- | _ -> assert false
+ | _ ->
+ [P.Note "not a theorem"]
(* interface functions ******************************************************)
in
let map i (direct, _) = mk_inverse i direct in
Array.iteri map b;
- out_table b;
+(* out_table b; *)
List.rev_map snd (List.tl (Array.to_list b)), rc
let aclassify t = classify (D.deannotate_term t)
in
let bobj =
CicNotationPres.box_of_mpres (
- CicNotationPres.render ids_to_uris (TermContentPres.pp_ast ast)
+ CicNotationPres.render ~prec:90 ids_to_uris
+ (TermContentPres.pp_ast ast)
)
in
let render = function _::x::_ -> x | _ -> assert false in
remove_closed_substs s
let obj_to_string n style prefix obj =
- let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in
+ let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
+ try Cic2acic.acic_object_of_cic_object obj
+ with e ->
+ let msg = "Cic2ACic: " ^ Printexc.to_string e in
+ failwith msg
+ in
match style with
| GrafiteAst.Declarative ->
let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
| Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
| Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
| Branch ([], s) -> a
- | Branch ([ps], s) -> render_steps a ps
+ | Branch ([ps], s) -> cont sep (render_steps a ps)
| Branch (pss, s) ->
let a = mk_ob :: a in
let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
function
| Absurd (_, term) -> "absurd" ^ term_pp term
- | Apply (_, term) -> "apply (" ^ term_pp term ^ ")" (* FG: rm parentheses *)
+ | Apply (_, term) -> "apply " ^ term_pp term
| ApplyS (_, term, params) ->
"applyS " ^ term_pp term ^
String.concat " "
| Constructor (_,n) -> "constructor " ^ string_of_int n
| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
- "cut (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *)
+ "cut " ^ term_pp term ^
(match ident with None -> "" | Some id -> " as " ^ id)
| Decompose (_, [], what, names) ->
sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names))
| Demodulate _ -> "demodulate"
| Destruct (_, term) -> "destruct " ^ term_pp term
| Elim (_, term, using, num, idents) ->
- sprintf "elim (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *)
+ sprintf "elim " ^ term_pp term ^
(match using with None -> "" | Some term -> " using " ^ term_pp term)
^ pp_intros_specs (num, idents)
| ElimType (_, term, using, num, idents) ->
(match ident_opt with None -> "" | Some ident -> " as " ^ ident)
| Left _ -> "left"
| LetIn (_, term, ident) ->
- sprintf "letin %s \\def %s" ident ("(" ^ term_pp term ^ ")") (* FG: rm parentheses *)
+ sprintf "letin %s \\def %s" ident (term_pp term)
| Reduce (_, kind, pat) ->
sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
| Reflexivity _ -> "reflexivity"
| Rewrite (_, pos, t, pattern, names) ->
sprintf "rewrite %s %s %s%s"
(if pos = `LeftToRight then ">" else "<")
- ("(" ^ term_pp t ^ ")") (* FG: rm parentheses *)
+ (term_pp t)
(pp_tactic_pattern pattern)
(if names = [] then "" else " as " ^ pp_idents names)
| Right _ -> "right"
set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/blt/defs".
-include "ext/preamble.ma".
+include "preamble.ma".
definition blt:
nat \to (nat \to bool)
set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/arith".
-include "ext/preamble.ma".
+include "preamble.ma".
theorem nat_dec:
\forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble".
-
-include' "../../../../legacy/coq.ma".
-
-(* FG: This is because "and" is a reserved keyword of the parser *)
-alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
-
-(* FG/CSC: These aliases should disappear: we would like to write something
- * like: "disambiguate in cic:/Coq/*"
- *)
-alias symbol "plus" = "Coq's natural plus".
-alias symbol "leq" = "Coq's natural 'less or equal to'".
-alias symbol "neq" = "Coq's not equal to (leibnitz)".
-alias symbol "eq" = "Coq's leibnitz's equality".
-
-alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
-alias id "conj" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1/1)".
-alias id "eq_add_S" = "cic:/Coq/Init/Peano/eq_add_S.con".
-alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
-alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
-alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
-alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
-alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con".
-alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)".
-alias id "ex_intro2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1/1)".
-alias id "false" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)".
-alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
-alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
-alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
-alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con".
-alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
-alias id "le_lt_n_Sm" = "cic:/Coq/Arith/Lt/le_lt_n_Sm.con".
-alias id "le_lt_or_eq" = "cic:/Coq/Arith/Lt/le_lt_or_eq.con".
-alias id "le_n" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)".
-alias id "le_n_O_eq" = "cic:/Coq/Arith/Le/le_n_O_eq.con".
-alias id "le_not_lt" = "cic:/Coq/Arith/Lt/le_not_lt.con".
-alias id "le_n_S" = "cic:/Coq/Arith/Le/le_n_S.con".
-alias id "le_O_n" = "cic:/Coq/Arith/Le/le_O_n.con".
-alias id "le_or_lt" = "cic:/Coq/Arith/Lt/le_or_lt.con".
-alias id "le_plus_l" = "cic:/Coq/Arith/Plus/le_plus_l.con".
-alias id "le_plus_minus" = "cic:/Coq/Arith/Minus/le_plus_minus.con".
-alias id "le_plus_minus_r" = "cic:/Coq/Arith/Minus/le_plus_minus_r.con".
-alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
-alias id "le_S" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/2)".
-alias id "le_S_n" = "cic:/Coq/Arith/Le/le_S_n.con".
-alias id "le_Sn_n" = "cic:/Coq/Arith/Le/le_Sn_n.con".
-alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
-alias id "lt" = "cic:/Coq/Init/Peano/lt.con".
-alias id "lt_irrefl" = "cic:/Coq/Arith/Lt/lt_irrefl.con".
-alias id "lt_le_S" = "cic:/Coq/Arith/Lt/lt_le_S.con".
-alias id "lt_n_S" = "cic:/Coq/Arith/Lt/lt_n_S.con".
-alias id "minus" = "cic:/Coq/Init/Peano/minus.con".
-alias id "minus_n_O" = "cic:/Coq/Arith/Minus/minus_n_O.con".
-alias id "minus_plus" = "cic:/Coq/Arith/Minus/minus_plus.con".
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias id "nat_ind" = "cic:/Coq/Init/Datatypes/nat_ind.con".
-alias id "not" = "cic:/Coq/Init/Logic/not.con".
-alias id "not_eq_S" = "cic:/Coq/Init/Peano/not_eq_S.con".
-alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
-alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
-alias id "or_ind" = "cic:/Coq/Init/Logic/or_ind.con".
-alias id "or_introl" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/1)".
-alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
-alias id "O_S" = "cic:/Coq/Init/Peano/O_S.con".
-alias id "plus_assoc" = "cic:/Coq/Arith/Plus/plus_assoc.con".
-alias id "plus_assoc_reverse" = "cic:/Coq/Arith/Plus/plus_assoc_reverse.con".
-alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
-alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
-alias id "plus_le_compat" = "cic:/Coq/Arith/Plus/plus_le_compat.con".
-alias id "plus_le_reg_l" = "cic:/Coq/Arith/Plus/plus_le_reg_l.con".
-alias id "plus_lt_reg_l" = "cic:/Coq/Arith/Plus/plus_lt_reg_l.con".
-alias id "plus_n_Sm" = "cic:/Coq/Init/Peano/plus_n_Sm.con".
-alias id "plus_reg_l" = "cic:/Coq/Arith/Plus/plus_reg_l.con".
-alias id "pred" = "cic:/Coq/Init/Peano/pred.con".
-alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
-alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
-alias id "true" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)".
-alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
-alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con".
-alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
-alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
-alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con".
-alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
-alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
-alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con".
-alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con".
-alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
-alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
-alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
-alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
-alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
-alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
-alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
-alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
-alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
-alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con".
-alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
-alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
-alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con".
-alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con".
-alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con".
-alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con".
-alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con".
-alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con".
-alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con".
-
-theorem f_equal: \forall A,B:Type. \forall f:A \to B.
- \forall x,y:A. x = y \to f x = f y.
- intros. elim H. reflexivity.
-qed.
-
-theorem sym_eq: \forall A:Type. \forall x,y:A. x = y \to y = x.
- intros. rewrite > H. reflexivity.
-qed.
-
-theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x.
- unfold not. intros. apply H. symmetry. assumption.
-qed.
-
-theorem trans_eq : ∀A:Type.∀x,y,z:A.x=y→y=z→x=z.
- intros;
- transitivity y;
- assumption.
-qed.
-
-theorem plus_reg_l: \forall (n,m,p:nat). n + m = n + p \to m = p.
- intros. apply plus_reg_l; auto.
-qed.
-
-theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m.
- intros. apply plus_le_reg_l; auto.
-qed.
-
-default "equality"
- cic:/Coq/Init/Logic/eq.ind
- cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/sym_eq.con
- cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/trans_eq.con
- cic:/Coq/Init/Logic/eq_ind.con
- cic:/Coq/Init/Logic/eq_ind_r.con
- cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/f_equal.con
- cic:/matita/legacy/coq/f_equal1.con.
set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/tactics".
-include "ext/preamble.ma".
+include "preamble.ma".
theorem insert_eq:
\forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G:
set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/plist/defs".
-include "ext/preamble.ma".
+include "preamble.ma".
inductive PList: Set \def
| PNil: PList
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble".
+
+include' "../../../../legacy/coq.ma".
+
+(* FG: This is because "and" is a reserved keyword of the parser *)
+alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
+
+(* FG/CSC: These aliases should disappear: we would like to write something
+ * like: "disambiguate in cic:/Coq/*"
+ *)
+alias symbol "plus" = "Coq's natural plus".
+alias symbol "leq" = "Coq's natural 'less or equal to'".
+alias symbol "neq" = "Coq's not equal to (leibnitz)".
+alias symbol "eq" = "Coq's leibnitz's equality".
+
+alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
+alias id "conj" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1/1)".
+alias id "eq_add_S" = "cic:/Coq/Init/Peano/eq_add_S.con".
+alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
+alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
+alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
+alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con".
+alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)".
+alias id "ex_intro2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1/1)".
+alias id "false" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)".
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
+alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
+alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con".
+alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
+alias id "le_lt_n_Sm" = "cic:/Coq/Arith/Lt/le_lt_n_Sm.con".
+alias id "le_lt_or_eq" = "cic:/Coq/Arith/Lt/le_lt_or_eq.con".
+alias id "le_n" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)".
+alias id "le_n_O_eq" = "cic:/Coq/Arith/Le/le_n_O_eq.con".
+alias id "le_not_lt" = "cic:/Coq/Arith/Lt/le_not_lt.con".
+alias id "le_n_S" = "cic:/Coq/Arith/Le/le_n_S.con".
+alias id "le_O_n" = "cic:/Coq/Arith/Le/le_O_n.con".
+alias id "le_or_lt" = "cic:/Coq/Arith/Lt/le_or_lt.con".
+alias id "le_plus_l" = "cic:/Coq/Arith/Plus/le_plus_l.con".
+alias id "le_plus_minus" = "cic:/Coq/Arith/Minus/le_plus_minus.con".
+alias id "le_plus_minus_r" = "cic:/Coq/Arith/Minus/le_plus_minus_r.con".
+alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
+alias id "le_S" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/2)".
+alias id "le_S_n" = "cic:/Coq/Arith/Le/le_S_n.con".
+alias id "le_Sn_n" = "cic:/Coq/Arith/Le/le_Sn_n.con".
+alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
+alias id "lt" = "cic:/Coq/Init/Peano/lt.con".
+alias id "lt_irrefl" = "cic:/Coq/Arith/Lt/lt_irrefl.con".
+alias id "lt_le_S" = "cic:/Coq/Arith/Lt/lt_le_S.con".
+alias id "lt_n_S" = "cic:/Coq/Arith/Lt/lt_n_S.con".
+alias id "minus" = "cic:/Coq/Init/Peano/minus.con".
+alias id "minus_n_O" = "cic:/Coq/Arith/Minus/minus_n_O.con".
+alias id "minus_plus" = "cic:/Coq/Arith/Minus/minus_plus.con".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "nat_ind" = "cic:/Coq/Init/Datatypes/nat_ind.con".
+alias id "not" = "cic:/Coq/Init/Logic/not.con".
+alias id "not_eq_S" = "cic:/Coq/Init/Peano/not_eq_S.con".
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
+alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
+alias id "or_ind" = "cic:/Coq/Init/Logic/or_ind.con".
+alias id "or_introl" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/1)".
+alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
+alias id "O_S" = "cic:/Coq/Init/Peano/O_S.con".
+alias id "plus_assoc" = "cic:/Coq/Arith/Plus/plus_assoc.con".
+alias id "plus_assoc_reverse" = "cic:/Coq/Arith/Plus/plus_assoc_reverse.con".
+alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
+alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
+alias id "plus_le_compat" = "cic:/Coq/Arith/Plus/plus_le_compat.con".
+alias id "plus_le_reg_l" = "cic:/Coq/Arith/Plus/plus_le_reg_l.con".
+alias id "plus_lt_reg_l" = "cic:/Coq/Arith/Plus/plus_lt_reg_l.con".
+alias id "plus_n_Sm" = "cic:/Coq/Init/Peano/plus_n_Sm.con".
+alias id "plus_reg_l" = "cic:/Coq/Arith/Plus/plus_reg_l.con".
+alias id "pred" = "cic:/Coq/Init/Peano/pred.con".
+alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
+alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
+alias id "true" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)".
+alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
+alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con".
+alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
+alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
+alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con".
+alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
+alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
+alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con".
+alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con".
+alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
+alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
+alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
+alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
+alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
+alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
+alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
+alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
+alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
+alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con".
+alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
+alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
+alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con".
+alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con".
+alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con".
+alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con".
+alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con".
+alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con".
+alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con".
+
+theorem f_equal: \forall A,B:Type. \forall f:A \to B.
+ \forall x,y:A. x = y \to f x = f y.
+ intros. elim H. reflexivity.
+qed.
+
+theorem sym_eq: \forall A:Type. \forall x,y:A. x = y \to y = x.
+ intros. rewrite > H. reflexivity.
+qed.
+
+theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x.
+ unfold not. intros. apply H. symmetry. assumption.
+qed.
+
+theorem trans_eq : ∀A:Type.∀x,y,z:A.x=y→y=z→x=z.
+ intros;
+ transitivity y;
+ assumption.
+qed.
+
+theorem plus_reg_l: \forall (n,m,p:nat). n + m = n + p \to m = p.
+ intros. apply plus_reg_l; auto.
+qed.
+
+theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m.
+ intros. apply plus_le_reg_l; auto.
+qed.
+
+default "equality"
+ cic:/Coq/Init/Logic/eq.ind
+ cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble/sym_eq.con
+ cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble/trans_eq.con
+ cic:/Coq/Init/Logic/eq_ind.con
+ cic:/Coq/Init/Logic/eq_ind_r.con
+ cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble/f_equal.con
+ cic:/matita/legacy/coq/f_equal1.con.
set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs".
-include "ext/preamble.ma".
+include "preamble.ma".
inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
| and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
| or4_intro2: P2 \to (or4 P0 P1 P2 P3)
| or4_intro3: P3 \to (or4 P0 P1 P2 P3).
-inductive ex3 (A0: Set) (P0: (A0 \to Prop)) (P1: (A0 \to Prop)) (P2: (A0 \to
-Prop)): Prop \def
+inductive ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to
+Prop): Prop \def
| ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0
P0 P1 P2)))).
-inductive ex4 (A0: Set) (P0: (A0 \to Prop)) (P1: (A0 \to Prop)) (P2: (A0 \to
-Prop)) (P3: (A0 \to Prop)): Prop \def
+inductive ex4 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to Prop)
+(P3: A0 \to Prop): Prop \def
| ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0)
\to (ex4 A0 P0 P1 P2 P3))))).
-inductive ex_2 (A0: Set) (A1: Set) (P0: (A0 \to (A1 \to Prop))): Prop \def
+inductive ex_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)): Prop \def
| ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1
P0))).
-inductive ex2_2 (A0: Set) (A1: Set) (P0: (A0 \to (A1 \to Prop))) (P1: (A0 \to
-(A1 \to Prop))): Prop \def
+inductive ex2_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
+(A1 \to Prop)): Prop \def
| ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
\to (ex2_2 A0 A1 P0 P1)))).
-inductive ex3_2 (A0: Set) (A1: Set) (P0: (A0 \to (A1 \to Prop))) (P1: (A0 \to
-(A1 \to Prop))) (P2: (A0 \to (A1 \to Prop))): Prop \def
+inductive ex3_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
+(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def
| ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
\to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))).
-inductive ex4_2 (A0: Set) (A1: Set) (P0: (A0 \to (A1 \to Prop))) (P1: (A0 \to
-(A1 \to Prop))) (P2: (A0 \to (A1 \to Prop))) (P3: (A0 \to (A1 \to Prop))):
-Prop \def
+inductive ex4_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
+(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)): Prop
+\def
| ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
\to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))).
-inductive ex_3 (A0: Set) (A1: Set) (A2: Set) (P0: (A0 \to (A1 \to (A2 \to
-Prop)))): Prop \def
+inductive ex_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
+Prop))): Prop \def
| ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1
x2) \to (ex_3 A0 A1 A2 P0)))).
-inductive ex2_3 (A0: Set) (A1: Set) (A2: Set) (P0: (A0 \to (A1 \to (A2 \to
-Prop)))) (P1: (A0 \to (A1 \to (A2 \to Prop)))): Prop \def
+inductive ex2_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
+Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def
| ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))).
-inductive ex3_3 (A0: Set) (A1: Set) (A2: Set) (P0: (A0 \to (A1 \to (A2 \to
-Prop)))) (P1: (A0 \to (A1 \to (A2 \to Prop)))) (P2: (A0 \to (A1 \to (A2 \to
-Prop)))): Prop \def
+inductive ex3_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
+Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to
+Prop))): Prop \def
| ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1
P2)))))).
-inductive ex4_3 (A0: Set) (A1: Set) (A2: Set) (P0: (A0 \to (A1 \to (A2 \to
-Prop)))) (P1: (A0 \to (A1 \to (A2 \to Prop)))) (P2: (A0 \to (A1 \to (A2 \to
-Prop)))) (P3: (A0 \to (A1 \to (A2 \to Prop)))): Prop \def
+inductive ex4_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
+Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to
+Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
| ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0
A1 A2 P0 P1 P2 P3))))))).
-inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: (A0 \to (A1 \to
-(A2 \to (A3 \to Prop))))) (P1: (A0 \to (A1 \to (A2 \to (A3 \to Prop))))) (P2:
-(A0 \to (A1 \to (A2 \to (A3 \to Prop))))): Prop \def
+inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to
+(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0
+\to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
| ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
(ex3_4 A0 A1 A2 A3 P0 P1 P2))))))).
-inductive ex4_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: (A0 \to (A1 \to
-(A2 \to (A3 \to Prop))))) (P1: (A0 \to (A1 \to (A2 \to (A3 \to Prop))))) (P2:
-(A0 \to (A1 \to (A2 \to (A3 \to Prop))))) (P3: (A0 \to (A1 \to (A2 \to (A3
-\to Prop))))): Prop \def
+inductive ex4_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to
+(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0
+\to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2 \to (A3 \to
+Prop)))): Prop \def
| ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))).
-inductive ex4_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: (A0
-\to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))) (P1: (A0 \to (A1 \to (A2 \to
-(A3 \to (A4 \to Prop)))))) (P2: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
-Prop)))))) (P3: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))): Prop \def
+inductive ex4_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to
+(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
+(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:
+A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
| ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1
P2 P3))))))))).
-inductive ex5_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: (A0
-\to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))) (P1: (A0 \to (A1 \to (A2 \to
-(A3 \to (A4 \to Prop)))))) (P2: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
-Prop)))))) (P3: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))) (P4: (A0
-\to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))): Prop \def
+inductive ex5_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to
+(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
+(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:
+A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4: A0 \to (A1 \to (A2 \to
+(A3 \to (A4 \to Prop))))): Prop \def
| ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to
(ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))).
inductive ex6_6 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set)
-(P0: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop))))))) (P1: (A0 \to
-(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop))))))) (P2: (A0 \to (A1 \to (A2
-\to (A3 \to (A4 \to (A5 \to Prop))))))) (P3: (A0 \to (A1 \to (A2 \to (A3 \to
-(A4 \to (A5 \to Prop))))))) (P4: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
-\to Prop))))))) (P5: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
-Prop))))))): Prop \def
+(P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1: A0 \to
+(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2: A0 \to (A1 \to (A2
+\to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to
+(A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
+\to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
+Prop)))))): Prop \def
| ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1
x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5)
A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))).
inductive ex6_7 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set)
-(A6: Set) (P0: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop)))))))) (P1: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop)))))))) (P2: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop)))))))) (P3: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop)))))))) (P4: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop)))))))) (P5: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
-Prop)))))))): Prop \def
+(A6: Set) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
+Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
+Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
+Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
+Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
+Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
+Prop))))))): Prop \def
| ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
(x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2
x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests".
+set "baseuri" "cic:/matita/test/prova".
-include "../contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma".
+include "../contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma".
alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
inline procedural
"cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".
+(*
+inline procedural
+ "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3/ty3_sred_wcpr0_pr0.con".
+
+inline procedural
+ "cic:/Coq/Reals/RiemannInt/FTC_Riemann.con".
+*)
projects / helm.git / commitdiff