*)
(* 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