proposition: Lemma inl_equivalence_prop S R: equivalence R -> (forall i j x, gle (isr S) i j -> inc x (Vg (isE S) i) -> related R (J x i) (J (Vf (Vg (isf S) (J i j)) x) j)) -> forall a b, related (inl_equiv S) a b -> related R a b.
proof: Proof. move => [_ _ p3 p4] hc a b /graph_on_P1 [ad bd [k [lik ljk]] sv]. move/(inl_sumP): ad => [a1 a2 a3]. move/(inl_sumP): bd => [b1 b2 b3]. move: (hc (Q a) k (P a) lik a3). move: (hc (Q b) k (P b) ljk b3). rewrite sv a1 b1 => r1 r2; exact: (p3 _ _ _ r2 (p4 _ _ r1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)