| unfold setoid1_of_setoid; simplify;
intros; split; intros 2; simplify in f ⊢ %; apply trans;
[ apply a |4: apply a'] try assumption; apply sym; assumption]
| unfold setoid1_of_setoid; simplify;
intros; split; intros 2; simplify in f ⊢ %; apply trans;
[ apply a |4: apply a'] try assumption; apply sym; assumption]