proposition: Lemma fold_right_eqlistA2 : forall s s' (i j:B) (heqij: eqB i j) (heqss': eqlistA s s'), eqB (fold_right f i s) (fold_right f j s').
proof: Proof. intros s. induction s as [|a s IHs];intros s' i j heqij heqss'. - inversion heqss'. subst. simpl. assumption. - inversion heqss'. subst. simpl. apply Comp. + assumption. + apply IHs;assumption. Qed.
imports: List Sorted Setoid Basics Morphisms