- transcript: patched to generate aliases instead of inlined variables

[helm.git] / matita / contribs / CoRN-Decl / ftc / RefLemma.ma

diff --git a/matita/contribs/CoRN-Decl/ftc/RefLemma.ma b/matita/contribs/CoRN-Decl/ftc/RefLemma.ma
index 9503e78c139b8b8d21492f1961d51b7705f22631..6034e5361c67c2ad1644410a752f60898512103b 100644 (file)
--- a/matita/contribs/CoRN-Decl/ftc/RefLemma.ma
+++ b/matita/contribs/CoRN-Decl/ftc/RefLemma.ma
@@ -27,7 +27,7 @@ include "ftc/RefSeparated.ma".
 include "ftc/RefSepRef.ma".
 
 (* UNEXPORTED
-Section Refinement_Lemma.
+Section Refinement_Lemma
 *)
 
 (*#* *The Refinement Lemmas
@@ -81,32 +81,32 @@ Using the results from these files, we prove our main lemma in several steps
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/RefLemma/a.var".
+alias id "a" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/a.var".
 
-inline "cic:/CoRN/ftc/RefLemma/b.var".
+alias id "b" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/b.var".
 
-inline "cic:/CoRN/ftc/RefLemma/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Hab.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/I.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/F.var".
+alias id "F" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/F.var".
 
-inline "cic:/CoRN/ftc/RefLemma/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF.var".
 
-inline "cic:/CoRN/ftc/RefLemma/incF.var".
+alias id "incF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/incF.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/contF'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__".
 
 (* end hide *)
 
 (* UNEXPORTED
-Section First_Refinement_Lemma.
+Section First_Refinement_Lemma
 *)
 
 (*#*
@@ -124,43 +124,43 @@ respectively.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/RefLemma/e.var".
+alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/e.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He.var".
+alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/He.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/d.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/m.var".
+alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/m.var".
 
-inline "cic:/CoRN/ftc/RefLemma/n.var".
+alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/n.var".
 
-inline "cic:/CoRN/ftc/RefLemma/P.var".
+alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/P.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HMesh.var".
+alias id "HMesh" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HMesh.var".
 
-inline "cic:/CoRN/ftc/RefLemma/Q.var".
+alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Q.var".
 
-inline "cic:/CoRN/ftc/RefLemma/Href.var".
+alias id "Href" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Href.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fP.var".
+alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP.var".
+alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
+alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fQ.var".
+alias id "fQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fQ.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfQ.var".
+alias id "HfQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfQ'.var".
+alias id "HfQ'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ'.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/sub.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_sub_0.con".
 
@@ -174,11 +174,11 @@ inline "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_sub_S.con".
 
-inline "cic:/CoRN/ftc/RefLemma/H.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__".
 
-inline "cic:/CoRN/ftc/RefLemma/H'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__".
 
-inline "cic:/CoRN/ftc/RefLemma/H0.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con".
 
@@ -223,11 +223,11 @@ inline "cic:/CoRN/ftc/RefLemma/ref_calc8.con".
 inline "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con".
 
 (* UNEXPORTED
-End First_Refinement_Lemma.
+End First_Refinement_Lemma
 *)
 
 (* UNEXPORTED
-Section Second_Refinement_Lemma.
+Section Second_Refinement_Lemma
 *)
 
 (*#*
@@ -246,62 +246,62 @@ and [R], respectively.
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/RefLemma/n.var".
+alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/n.var".
 
-inline "cic:/CoRN/ftc/RefLemma/j.var".
+alias id "j" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/j.var".
 
-inline "cic:/CoRN/ftc/RefLemma/k.var".
+alias id "k" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/k.var".
 
-inline "cic:/CoRN/ftc/RefLemma/P.var".
+alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/P.var".
 
-inline "cic:/CoRN/ftc/RefLemma/Q.var".
+alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/Q.var".
 
-inline "cic:/CoRN/ftc/RefLemma/R.var".
+alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/R.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HrefP.var".
+alias id "HrefP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HrefR.var".
+alias id "HrefR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/e.var".
+alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e.var".
 
-inline "cic:/CoRN/ftc/RefLemma/e'.var".
+alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He.var".
+alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He'.var".
+alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He'.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/d.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__".
 
-inline "cic:/CoRN/ftc/RefLemma/d'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
+alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
+alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fP.var".
+alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP.var".
+alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
+alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fR.var".
+alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfR.var".
+alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
+alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR'.var".
 
 inline "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con".
 
 (* UNEXPORTED
-End Second_Refinement_Lemma.
+End Second_Refinement_Lemma
 *)
 
 (* UNEXPORTED
-Section Third_Refinement_Lemma.
+Section Third_Refinement_Lemma
 *)
 
 (*#*
@@ -320,109 +320,109 @@ respectively;
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/RefLemma/n.var".
+alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/n.var".
 
-inline "cic:/CoRN/ftc/RefLemma/m.var".
+alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/m.var".
 
-inline "cic:/CoRN/ftc/RefLemma/P.var".
+alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P.var".
 
-inline "cic:/CoRN/ftc/RefLemma/R.var".
+alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R.var".
 
-inline "cic:/CoRN/ftc/RefLemma/e.var".
+alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e.var".
 
-inline "cic:/CoRN/ftc/RefLemma/e'.var".
+alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He.var".
+alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He'.var".
+alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He'.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/d.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
-inline "cic:/CoRN/ftc/RefLemma/d'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
+alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
+alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fP.var".
+alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP.var".
+alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
+alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fR.var".
+alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfR.var".
+alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
+alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/Hab'.var".
+alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hab'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/beta.var".
+alias id "beta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/beta.var".
 
-inline "cic:/CoRN/ftc/RefLemma/Hbeta.var".
+alias id "Hbeta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hbeta.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/alpha.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_alpha.con".
 
-inline "cic:/CoRN/ftc/RefLemma/csi1.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_csi1.con".
 
-inline "cic:/CoRN/ftc/RefLemma/delta1.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_delta1.con".
 
-inline "cic:/CoRN/ftc/RefLemma/P'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con".
 
-inline "cic:/CoRN/ftc/RefLemma/fP'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con".
 
-inline "cic:/CoRN/ftc/RefLemma/csi2.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_csi2.con".
 
-inline "cic:/CoRN/ftc/RefLemma/delta2.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_delta2.con".
 
-inline "cic:/CoRN/ftc/RefLemma/R'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con".
 
-inline "cic:/CoRN/ftc/RefLemma/fR'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con".
 
-inline "cic:/CoRN/ftc/RefLemma/csi3.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_csi3.con".
 
-inline "cic:/CoRN/ftc/RefLemma/Q.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con".
 
-inline "cic:/CoRN/ftc/RefLemma/fQ.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 
 inline "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con".
 
@@ -433,16 +433,16 @@ inline "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con".
 inline "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con".
 
 (* UNEXPORTED
-End Third_Refinement_Lemma.
+End Third_Refinement_Lemma
 *)
 
 (* UNEXPORTED
-Section Fourth_Refinement_Lemma.
+Section Fourth_Refinement_Lemma
 *)
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/Fa.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
 
 (* NOTATION
 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
@@ -457,111 +457,111 @@ Finally, this is inequality (2.6.7) exactly as stated (same conventions as
 above)
 *)
 
-inline "cic:/CoRN/ftc/RefLemma/n.var".
+alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/n.var".
 
-inline "cic:/CoRN/ftc/RefLemma/m.var".
+alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/m.var".
 
-inline "cic:/CoRN/ftc/RefLemma/P.var".
+alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/P.var".
 
-inline "cic:/CoRN/ftc/RefLemma/R.var".
+alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/R.var".
 
-inline "cic:/CoRN/ftc/RefLemma/e.var".
+alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e.var".
 
-inline "cic:/CoRN/ftc/RefLemma/e'.var".
+alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He.var".
+alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He'.var".
+alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He'.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/d.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
 
-inline "cic:/CoRN/ftc/RefLemma/d'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
+alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
+alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fP.var".
+alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP.var".
+alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
+alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fR.var".
+alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfR.var".
+alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
+alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR'.var".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/RefLemma/Hab'.var".
+alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Hab'.var".
 
 (* end show *)
 
 inline "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con".
 
 (* UNEXPORTED
-End Fourth_Refinement_Lemma.
+End Fourth_Refinement_Lemma
 *)
 
 (* UNEXPORTED
-Section Main_Refinement_Lemma.
+Section Main_Refinement_Lemma
 *)
 
 (*#* We finish by presenting Theorem 9. *)
 
-inline "cic:/CoRN/ftc/RefLemma/n.var".
+alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/n.var".
 
-inline "cic:/CoRN/ftc/RefLemma/m.var".
+alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/m.var".
 
-inline "cic:/CoRN/ftc/RefLemma/P.var".
+alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/P.var".
 
-inline "cic:/CoRN/ftc/RefLemma/R.var".
+alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/R.var".
 
-inline "cic:/CoRN/ftc/RefLemma/e.var".
+alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e.var".
 
-inline "cic:/CoRN/ftc/RefLemma/e'.var".
+alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He.var".
+alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He.var".
 
-inline "cic:/CoRN/ftc/RefLemma/He'.var".
+alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He'.var".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/d.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__".
 
-inline "cic:/CoRN/ftc/RefLemma/d'.con".
+inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
+alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
+alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fP.var".
+alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP.var".
+alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
+alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP'.var".
 
-inline "cic:/CoRN/ftc/RefLemma/fR.var".
+alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfR.var".
+alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR.var".
 
-inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
+alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR'.var".
 
 inline "cic:/CoRN/ftc/RefLemma/refinement_lemma.con".
 
 (* UNEXPORTED
-End Main_Refinement_Lemma.
+End Main_Refinement_Lemma
 *)
 
 (* UNEXPORTED
-End Refinement_Lemma.
+End Refinement_Lemma
 *)