Section Lemma1
*)
-inline "cic:/CoRN/ftc/WeakIVT/Lemma1/a.var" "Lemma1__".
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/Lemma1/a.var".
-inline "cic:/CoRN/ftc/WeakIVT/Lemma1/b.var" "Lemma1__".
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/Lemma1/b.var".
-inline "cic:/CoRN/ftc/WeakIVT/Lemma1/Hab.var" "Lemma1__".
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/Lemma1/Hab.var".
(* begin hide *)
(* end hide *)
-inline "cic:/CoRN/ftc/WeakIVT/Lemma1/F.var" "Lemma1__".
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/Lemma1/F.var".
-inline "cic:/CoRN/ftc/WeakIVT/Lemma1/contF.var" "Lemma1__".
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/Lemma1/contF.var".
(*#* **First Lemmas
Section Lemma2
*)
-inline "cic:/CoRN/ftc/WeakIVT/Lemma2/a.var" "Lemma2__".
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/Lemma2/a.var".
-inline "cic:/CoRN/ftc/WeakIVT/Lemma2/b.var" "Lemma2__".
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/Lemma2/b.var".
-inline "cic:/CoRN/ftc/WeakIVT/Lemma2/Hab.var" "Lemma2__".
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/Lemma2/Hab.var".
(* begin hide *)
(* end hide *)
-inline "cic:/CoRN/ftc/WeakIVT/Lemma2/F.var" "Lemma2__".
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/Lemma2/F.var".
-inline "cic:/CoRN/ftc/WeakIVT/Lemma2/contF.var" "Lemma2__".
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/Lemma2/contF.var".
(*#*
If [f(b) [<] f(a)], a similar result holds:
converge to [x0] such that [f(x0) [=] z].
*)
-inline "cic:/CoRN/ftc/WeakIVT/IVT/a.var" "IVT__".
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/IVT/a.var".
-inline "cic:/CoRN/ftc/WeakIVT/IVT/b.var" "IVT__".
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/IVT/b.var".
-inline "cic:/CoRN/ftc/WeakIVT/IVT/Hab'.var" "IVT__".
+alias id "Hab'" = "cic:/CoRN/ftc/WeakIVT/IVT/Hab'.var".
-inline "cic:/CoRN/ftc/WeakIVT/IVT/Hab.var" "IVT__".
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/IVT/Hab.var".
(* begin hide *)
(* end hide *)
-inline "cic:/CoRN/ftc/WeakIVT/IVT/F.var" "IVT__".
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/IVT/F.var".
-inline "cic:/CoRN/ftc/WeakIVT/IVT/contF.var" "IVT__".
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/IVT/contF.var".
(* begin hide *)
(* begin show *)
-inline "cic:/CoRN/ftc/WeakIVT/IVT/incrF.var" "IVT__".
+alias id "incrF" = "cic:/CoRN/ftc/WeakIVT/IVT/incrF.var".
(* end show *)
(* begin show *)
-inline "cic:/CoRN/ftc/WeakIVT/IVT/z.var" "IVT__".
+alias id "z" = "cic:/CoRN/ftc/WeakIVT/IVT/z.var".
-inline "cic:/CoRN/ftc/WeakIVT/IVT/Haz.var" "IVT__".
+alias id "Haz" = "cic:/CoRN/ftc/WeakIVT/IVT/Haz.var".
-inline "cic:/CoRN/ftc/WeakIVT/IVT/Hzb.var" "IVT__".
+alias id "Hzb" = "cic:/CoRN/ftc/WeakIVT/IVT/Hzb.var".
(* end show *)