inline "cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con".
+(* NOTATION
+Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
+*)
+
+(* NOTATION
+Notation just2 :=
+ (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)).
+*)
+
inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con".
inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con".