proposition: Lemma FunctExt_BijComp : FunctionalExtensionality -> BijectivityBijectiveComp.
proof: Proof. intros FunExt * (Hgf,Hfg). split; unfold action. - intros h; apply FunExt; intro b; rewrite Hfg; reflexivity. - intros h; apply FunExt; intro a; rewrite Hgf; reflexivity. Qed.