proposition: Lemma ex6_prop5d i j (H:gle rL i j): inl_same_data (ex6_systemi i) (inl_restr (ex6_prop5c H)).
proof: Proof. move:(arg1_sr H) (arg2_sr H); rewrite HLs => iL jL. move: (HJm H) => ss. rewrite /inl_same_data. simpl. move:(ex6_prop5b iL)(ex6_prop5b jL) => [-> _ -> ->] [-> _ -> ->]. rewrite (iorder_trans _ ss) (double_restr _ ss) double_restr //. by move => p /setI2_P [ha hb]; apply/setI2_P; split => //;apply:(setX_Sll ss). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)