exfalso
case inr.inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ sign (transpos i j) = true
case inr.inl.h
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ False