set "baseuri" "cic:/matita/CoRN-Decl/fta/KeyLemma".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: KeyLemma.v,v 1.5 2004/04/23 10:00:57 lcf Exp $ *)
*)
(* UNEXPORTED
-Section Key_Lemma.
+Section Key_Lemma
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/fta/KeyLemma/a.var".
+alias id "a" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a.var".
-inline "cic:/CoRN/fta/KeyLemma/n.var".
+alias id "n" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/n.var".
-inline "cic:/CoRN/fta/KeyLemma/gt_n_0.var".
+alias id "gt_n_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/gt_n_0.var".
-inline "cic:/CoRN/fta/KeyLemma/eps.var".
+alias id "eps" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps.var".
-inline "cic:/CoRN/fta/KeyLemma/eps_pos.var".
+alias id "eps_pos" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_pos.var".
-inline "cic:/CoRN/fta/KeyLemma/a_nonneg.var".
+alias id "a_nonneg" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_nonneg.var".
-inline "cic:/CoRN/fta/KeyLemma/a_n_1.var".
+alias id "a_n_1" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_n_1.var".
-inline "cic:/CoRN/fta/KeyLemma/a_0.var".
+alias id "a_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_0.var".
-inline "cic:/CoRN/fta/KeyLemma/eps_le_a_0.var".
+alias id "eps_le_a_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_le_a_0.var".
inline "cic:/CoRN/fta/KeyLemma/a_0_eps_nonneg.con".
(* end hide *)
(* UNEXPORTED
-End Key_Lemma.
+End Key_Lemma
*)
(* UNEXPORTED