proposition: Lemma BijComp_FunctExt : BijectivityBijectiveComp -> FunctionalExtensionality.
proof: Proof. intros BijComp. apply FunctExt_iff_UniqInverse. intros * H1 H2. destruct BijComp with (C:=A) (1:=H2) as (Hg2f,_). destruct BijComp with (C:=A) (1:=H1) as (_,Hfg1). rewrite <- (Hg2f g1). change g1 with (action g1 (fun x => x)). rewrite -> (Hfg1 (fun x => x)). reflexivity. Qed.