]>
matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/algebra/finite_groups.ma
[ simplify in H5;
clear Hcut;
clear Hcut1;
+ unfold f' in H5;
clear f';
elim H5;
clear H5;
[ simplify in H5;
clear Hcut;
clear Hcut1;
+ unfold f' in H5;
clear f';
elim H5;
clear H5;
assumption
]
| intros;
+ unfold f;
apply index_of_sur
]
].