proposition: Lemma MirrorMap (X Y:Type) : forall (f: X -> Y) s, (Mirror (Map f s)) = (Map f (Mirror s)).
proof: Proof. intros f. induction s. reflexivity. change (Mirror (glue o (Map f s1) (Map f s2)) = glue (OpenUnitDual o) (Map f (Mirror s2)) (Map f (Mirror s1))). rewrite <- IHs1. rewrite <- IHs2. reflexivity. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields