Goal:
  
  A : Type
  B : Type
  P : A → B → Prop
  P' : ∀ (a : A) (b : B), P a b → Prop
  t : A
  t' : B
  ============================
   (None = Some t
    → ∀ H2 : None = Some t',
        P' t t'
          (False_ind (P t t')
             (eq_ind None
                (λ e : option B,
                   match e with
                   | Some _ => False
                   | None => True
                   end) I (Some t') H2)))


DEBUG:Going to execute:
congruence