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.