Section Well_foundedT
*)
-inline "cic:/CoRN/algebra/Basics/Well_foundedT/A.var" "Well_foundedT__".
+alias id "A" = "cic:/CoRN/algebra/Basics/Well_foundedT/A.var".
-inline "cic:/CoRN/algebra/Basics/Well_foundedT/R.var" "Well_foundedT__".
+alias id "R" = "cic:/CoRN/algebra/Basics/Well_foundedT/R.var".
(*#* The accessibility predicate is defined to be non-informative *)
Section AccT
*)
-inline "cic:/CoRN/algebra/Basics/AccT/A.var" "AccT__".
+alias id "A" = "cic:/CoRN/algebra/Basics/AccT/A.var".
inline "cic:/CoRN/algebra/Basics/well_founded.con".
Section IndT
*)
-inline "cic:/CoRN/algebra/Basics/IndT/A.var" "IndT__".
+alias id "A" = "cic:/CoRN/algebra/Basics/IndT/A.var".
-inline "cic:/CoRN/algebra/Basics/IndT/R.var" "IndT__".
+alias id "R" = "cic:/CoRN/algebra/Basics/IndT/R.var".
(* UNEXPORTED
Section AccIter
*)
-inline "cic:/CoRN/algebra/Basics/IndT/AccIter/P.var" "IndT__AccIter__".
+alias id "P" = "cic:/CoRN/algebra/Basics/IndT/AccIter/P.var".
-inline "cic:/CoRN/algebra/Basics/IndT/AccIter/F.var" "IndT__AccIter__".
+alias id "F" = "cic:/CoRN/algebra/Basics/IndT/AccIter/F.var".
inline "cic:/CoRN/algebra/Basics/Acc_inv.con".
End AccIter
*)
-inline "cic:/CoRN/algebra/Basics/IndT/Rwf.var" "IndT__".
+alias id "Rwf" = "cic:/CoRN/algebra/Basics/IndT/Rwf.var".
inline "cic:/CoRN/algebra/Basics/well_founded_induction_type.con".
Section InductionT
*)
-inline "cic:/CoRN/algebra/Basics/InductionT/A.var" "InductionT__".
+alias id "A" = "cic:/CoRN/algebra/Basics/InductionT/A.var".
-inline "cic:/CoRN/algebra/Basics/InductionT/f.var" "InductionT__".
+alias id "f" = "cic:/CoRN/algebra/Basics/InductionT/f.var".
inline "cic:/CoRN/algebra/Basics/ltof.con".