proposition: Lemma ex5_res2 x j: ex5_coherent2 x -> inc j (psI S) -> domain x = emptyset -> exists x', ex5_extend_prop x j x'.
proof: Proof. move => [[ha hb hc] _ _] jI je. move:(ex5_G3 jI) =>[x' x'G]. have jj: ~inc j (domain x) by rewrite je => /in_set0. set J := domain x. have ha': fgraph (ex5_extend x j x') by apply:fgraph_setU1. have hb': domain (ex5_extend x j x') = J +s1 j by rewrite /J domain_setU1 . have vv: (Vg (ex5_extend x j x') j) = x' by rewrite setU1_V_out //. have vg: inc (Vg (ex5_extend x j x') j) (Vg Gf j) by rewrite vv. have dd: domain (ex5_extend x j x') = singleton j by rewrite hb' /J je set0_U2. have sdx: sub (domain (ex5_extend x j x')) (psI S). by rewrite dd => t /set1_P ->. have co: ex5_prodG (domain (ex5_extend x j x')) (ex5_extend x j x'). by rewrite dd;split => // i /set1_P ->; rewrite vv. exists x'; split=> // K [fsK neK];rewrite hb' /J je set0_U2 => /subset1P; case. by move => ke;case/nonemptyP: neK. move ->. have: (restr (ex5_extend x j x') (singleton j)) = (ex5_extend x j x'). by rewrite -{2} (restr_to_domain ha' (@sub_refl (ex5_extend x j x'))) dd. move ->;split. - split;[ by move => t /set1_P -> | apply:set1_finite | fprops ]. - by split; [ | | move => i /set1_P -> ]. - move => j1 j2 /set1_P -> /set1_P -> lee; rewrite vv. by rewrite /ex5_f (ps_identity_f jI) idV//; apply:(ex5_G4 jI). - move => k kip; move:((proj2 kip) _ (set1_1 j)) => lejk. move:(ex5_Gij_prop2 lejk x'G)=> [t ta tb]. have nej: nonempty (singleton j) by fprops. exists t; apply/setI2_P; split => //; apply/(ex5_Y_prop2 _ nej kip). split; first by apply:(ex5_G4 (proj1 kip)). by move => i /set1_P ->; rewrite vv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)