The manual proof style was nice to see for pedagogical purposes, however it should be noted that the statement is just a intuitionistic tautology, so much so th

The manual proof style was nice to see for pedagogical purposes, however it should be noted that the statement is just a intuitionistic tautology, so much so that the entire proof can be automated with the built-in firstorder tactic: Theorem impl_trait_transform: forall (Trait: Type -> Prop) (Result: Prop), ((exists t, Trait(t)) -> Result) <-> (forall t, (Trait(t) -> Result)). Proof. firstorder. Qed.