inline "cic:/CoRN/ftc/RefLemma/RL_g.con".
+(* NOTATION
+Notation g := RL_g.
+*)
+
+(* NOTATION
+Notation h := RL_h.
+*)
+
inline "cic:/CoRN/ftc/RefLemma/ref_calc1.con".
+(* NOTATION
+Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
+*)
+
+(* NOTATION
+Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
+*)
+
inline "cic:/CoRN/ftc/RefLemma/ref_calc2.con".
inline "cic:/CoRN/ftc/RefLemma/ref_calc3.con".
inline "cic:/CoRN/ftc/RefLemma/Fa.con".
+(* NOTATION
+Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
+*)
+
inline "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con".
(* end hide *)