proposition: Theorem eq_id_comm_l A (f:A->A) (Hf:forall a, a = f a) a : f_equal f (Hf a) = Hf (f a).
proof: Proof. unfold f_equal. rewrite <- (eq_trans_sym_inv_l (Hf a)). destruct (Hf a) at 1 2. destruct (Hf a). reflexivity. Defined.
imports: Notations Ltac