proposition: Lemma noid_inl_class_ii i x (y := Vf (Vg f (J i i)) x): inc i I -> inc x (Vg E i) -> [/\ inc y (Vg noid_E' i), inc (J x i) noid_inl_sum, inc (J y i) noid_inl_sum & class noid_inl_equiv (J x i) = class noid_inl_equiv (J y i)].
proof: Proof. move => iI xEi. have iir: inc (J i i) r by apply:(proj32 preorder_r); ue. case:(function_f iir); aw=> [fii sii tii]. have yE: inc y (Vg E i) by rewrite /y ; Wtac. have yE': inc y (Vg noid_E' i). by rewrite / noid_E' LgV//; apply/(Imf_P fii); exists x => //; ue. have xS: inc (J x i) noid_inl_sum. apply/noid_inl_sumP; split;aww. have yS: inc (J y i) noid_inl_sum. apply/noid_inl_sumP; split;aww. split => //; apply/(noid_inl_class_eq xS yS). by exists i; aw;split => //; rewrite -(noid_prop5g iir iir xEi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)