Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / ftc / RefLemma.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/RefLemma.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/RefLemma.mma
index 12ea49f4d81fa863fe6da7ca31126d50e7a35c7b..6fa5d117cdf276cf909db52351b13e55efaf484f 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/RefLemma.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/RefLemma.mma
@@ -87,7 +87,7 @@ alias id "Hab" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Hab.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__" as definition.
 
 (* end hide *)
 
@@ -99,7 +99,7 @@ alias id "incF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/incF.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__" as definition.
 
 (* end hide *)
 
@@ -128,7 +128,7 @@ alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 
 (* end hide *)
 
@@ -158,31 +158,31 @@ alias id "HfQ'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemm
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_0.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_0.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_n.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_S.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_S.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_h.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_h.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_g.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_g.con" as definition.
 
 (* NOTATION
 Notation g := RL_g.
@@ -192,7 +192,7 @@ Notation g := RL_g.
 Notation h := RL_h.
 *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc1.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc1.con" as lemma.
 
 (* NOTATION
 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
@@ -202,23 +202,23 @@ Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
 *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc2.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc3.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc3.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc4.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc4.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc5.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc5.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc6.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc6.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc7.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc7.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc8.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc8.con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con" as lemma.
 
 (* UNEXPORTED
 End First_Refinement_Lemma
@@ -270,9 +270,9 @@ alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemm
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__" as definition.
 
 (* end hide *)
 
@@ -292,7 +292,7 @@ alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemm
 
 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR'.var".
 
-inline procedural "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con" as lemma.
 
 (* UNEXPORTED
 End Second_Refinement_Lemma
@@ -336,9 +336,9 @@ alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
 (* end hide *)
 
@@ -366,69 +366,69 @@ alias id "Hbeta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lem
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_alpha.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_alpha.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi1.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta1.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi2.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta2.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi3.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi3.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con" as lemma.
 
 (* UNEXPORTED
 End Third_Refinement_Lemma
@@ -440,13 +440,13 @@ Section Fourth_Refinement_Lemma
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
 
 (* NOTATION
 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
 *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con" as lemma.
 
 (* end hide *)
 
@@ -473,9 +473,9 @@ alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemm
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
 
 (* end hide *)
 
@@ -501,7 +501,7 @@ alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lem
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con" as lemma.
 
 (* UNEXPORTED
 End Fourth_Refinement_Lemma
@@ -531,9 +531,9 @@ alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__" as definition.
 
-inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__".
+inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__" as definition.
 
 (* end hide *)
 
@@ -553,7 +553,7 @@ alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/
 
 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR'.var".
 
-inline procedural "cic:/CoRN/ftc/RefLemma/refinement_lemma.con".
+inline procedural "cic:/CoRN/ftc/RefLemma/refinement_lemma.con" as lemma.
 
 (* UNEXPORTED
 End Main_Refinement_Lemma