proposition: Lemma cpoly_map_strext : fun_strext cpoly_map_fun.
proof: Proof. intros x. induction x; intros y H. induction y. elim H. destruct H as [H|H]. left. eapply rh_apzero; apply H. right. apply IHy. apply H. destruct y as [|c y]. destruct H as [H|H]. left. eapply rh_apzero; apply H. right. change ([0][#]x). apply ap_symmetric. apply IHx. apply ap_symmetric. apply H. destruct H as [H|H]. left. eapply rh_strext; apply H. right. apply IHx. apply H. Defined.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational