- abstract (intros;
- destruct a; destruct b; destruct s; destruct s0; simpl in *;
- subst; simpl; set (F_full x1 x2 f) as ff1; set (F_full x1 x2 f') as ff2; destruct ff1; destruct ff2;
- apply F_faithful;
- etransitivity; [ apply e | idtac ];
- symmetry;
- etransitivity; [ apply e0 | idtac ];
- symmetry; auto).
- abstract (intros;
- simpl;
- destruct a as [ a1 [ a2 a3 ] ];
- subst;
- simpl;
- apply ff_functor_section_id_preserved).
- abstract (intros;
- destruct a as [ a1 [ a2 a3 ] ];
- destruct b as [ b1 [ b2 b3 ] ];
- destruct c as [ c1 [ c2 c3 ] ];
- subst;
- simpl in *;
- simpl in *;
- apply ff_functor_section_respectful).
+ intros.
+ unfold ff_functor_section_fmor; simpl.
+ destruct (F_full a b f).
+ destruct (F_full a b f').
+ apply F_faithful.
+ setoid_rewrite e0.
+ setoid_rewrite e.
+ auto.
+ intros; simpl; subst.
+ apply ff_functor_section_id_preserved.
+ intros; simpl in *.
+ apply ff_functor_section_respectful.