Well, I'm not sure if this is the best solution, but when faced with problems like this, you usually look around the context to see where you can get ⊥
and try to prove a property that leads to it.
Specially, you can't pattern match on t
because, as you said, τ′ ≠ τ₁
(which is one of your assumptions). But looking at the definition of tLam
, it should be possible to prove that:
lam-T≡ : ∀ {n τ₁ τ₂ τ′} {Γ : Ctxt n} {E : Expr (suc n)} →
Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂) → τ′ ≡ τ₁
And indeed, this is the case:
lam-T≡ (tLam t) = refl
This gives you a proof that ¬p
needs:
lem : ¬ Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂)
lem t = ¬p (lam-T≡ t)