title: Proving a theorem using equality relation: ∀[ x ] ∀[ y ] (¬ Eq x y → ¬ Eq (f x) (f y))
body: <p>I am trying to solve the following first order logic problem using Agda:</p>
  
  <pre><code>  problem : {A B : Set} {f : A → B} → inj f → ∀[ x ] ∀[ y ] (¬ Eq x y → ¬ Eq (f x) (f y))
  </code></pre>
  
  <p>using the following definitions of equality relations and some supporting defintions:</p>
  
  <pre><code>data ⊥ : Set where
  
  ⊥-elim : {A : Set} → ⊥ → A
  ⊥-elim ()
  
  infix 3 ¬_ 
  ¬_ : Set → Set
  ¬ A = A → ⊥
  
  Π : (A : Set) → (B : A → Set) → Set
  Π A B = (a : A) → B a
  
  forAll : {A : Set} → (B : A → Set) → Set
  forAll {A} B = Π A B
  
  ∀-syntax = forAll
  infix 0 ∀-syntax
  syntax ∀-syntax (λ a → B) = ∀[ a ] B
  
  apply : {A : Set} → {B : A → Set} → Π A B → (a : A) → B a
  apply f x = f x
  
  data Σ (A : Set) (B : A → Set) : Set where
      ⟨_,_⟩ : (a : A) → B a → Σ A B
  
  thereExists : ∀ {A : Set} (B : A → Set) → Set
  thereExists {A} B = Σ A B
  
  ∃-syntax = thereExists
  infix 0 ∃-syntax
  syntax ∃-syntax (λ x → B) = ∃[ x ] B
  
  ∃-elim : {A : Set} {B : A → Set} {C : Set} → (∀ (a : A) → B a → C) → Σ A B → C
  ∃-elim a→b→c ⟨ a , b ⟩ = a→b→c a b
  
  dfst : {A : Set} {B : A → Set} → Σ A B → A
  dfst ⟨ a , _ ⟩ = a
  
  dsnd : {A : Set} {B : A → Set} → (p : Σ A B) → B (dfst p)
  dsnd ⟨ _ , b ⟩ = b
  
  module IFOL 
      (Eq : {A : Set} → A → A → Set) 
      (subst : {A B : Set} → (f : A → B) → ∀[ a1 ] ∀[ a2 ] (Eq a1 a2 → Eq (f a1) (f a2))) 
      (trans : {A : Set} → (a1 a2 a3 : A) → Eq a1 a2 → Eq a2 a3 → Eq a1 a3) 
    where
  
    inj : {A B : Set} → (A → B) → Set
    inj {A} {B} f = ∀[ a1 ] ∀[ a2 ] (Eq (f a1) (f a2) → Eq a1 a2)
  
    surj : {A B : Set} → (A → B) → Set
    surj {A} {B} f = ∀[ b ] ∃[ a ] Eq (f a) b
  
    infix 20 _∘_
    _∘_ : {A B C : Set} → (A → B) → (B → C) → A → C
    (f ∘ g) a = g (f a)
  </code></pre>
  
  <p>My approach to solve it has been the following:</p>
  
  <pre><code>problem : {A B : Set} {f : A → B} → inj f → ∀[ x ] ∀[ y ] (¬ Eq x y → ¬ Eq (f x) (f y))
  problem injf x y noteqxy eqfxfy = noteqxy ?
  </code></pre>
  
  <p>However, I am stuck in there and can't work out further a solution that will let me get the goal <code>Eq x y</code>. I've tried using <code>injf</code> function in multiple ways but the main problem seems to be that I don't know how to return a function type.</p>
  
  <p>As this is a student assignment I am working on, I am not asking for a solution, only for a guidance as to how I should progress with that solution (is this the right direction? should I use <code>subst</code> or <code>trans</code> in my solution?).</p>