constructor
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ ((⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true) ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        curr + 1 ≤ idx →
          ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
                ref := (input.getRef idx hidx1).cast ⋯ },
              assign⟧ =
            true) ↔
    ⟦{ aig := aig, ref := acc }, assign⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true
case isTrue.mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ ((⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true) ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        curr + 1 ≤ idx →
          ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
                ref := (input.getRef idx hidx1).cast ⋯ },
              assign⟧ =
            true) →
    ⟦{ aig := aig, ref := acc }, assign⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true

case isTrue.mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
acc : aig.Ref
curr : Nat
hcurr : curr ≤ len
input : aig.RefStream len
res : Entrypoint α
h✝ : curr < len
hgo :
  go (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig
      (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).ref (curr + 1) len (input.cast ⋯) mkAndCached =
    res
⊢ (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧
      ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦{ aig := aig, ref := input.getRef idx hidx1 }, assign⟧ = true) →
    (⟦{ aig := aig, ref := acc }, assign⟧ = true ∧ ⟦{ aig := aig, ref := input.getRef curr h✝ }, assign⟧ = true) ∧
      ∀ (idx : Nat) (hidx1 : idx < len),
        curr + 1 ≤ idx →
          ⟦{ aig := (aig.mkAndCached { lhs := acc, rhs := input.getRef curr h✝ }).aig,
                ref := (input.getRef idx hidx1).cast ⋯ },
              assign⟧ =
            true