proposition: Theorem eq_id_comm_r A (f:A->A) (Hf:forall a, f a = a) a : f_equal f (Hf a) = Hf (f a).
proof: Proof. unfold f_equal. rewrite <- (eq_trans_sym_inv_l (Hf (f (f a)))). set (Hfsymf := fun a => eq_sym (Hf a)). change (eq_sym (Hf (f (f a)))) with (Hfsymf (f (f a))). pattern (Hfsymf (f (f a))). destruct (eq_id_comm_l f Hfsymf (f a)). destruct (eq_id_comm_l f Hfsymf a). unfold Hfsymf. destruct (Hf a). simpl. rewrite eq_trans_refl_l. reflexivity. Defined.
imports: Notations Ltac