cases a with
| inl =>
  cases b with
  | inl =>
    dsimp [inj] at h
    apply congrArg
    apply Nat.add_left_cancel
    exact h
  | inr rhs =>
    exfalso
    dsimp [inj] at h
    have := rhs.isLt
    omega
| inr lhs =>
  cases b with
  | inl =>
    exfalso
    dsimp [inj] at h
    have := lhs.isLt
    omega
  | inr =>
    dsimp [inj] at h
    apply congrArg
    apply Fin.eq_of_val_eq
    exact h
aig : AIG Nat
a b : aig.CNFVar
h : inj a = inj b
⊢ a = b
no goals