-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.eq_def : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVLogicalExpr)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache =
    match expr with
    | Std.Tactic.BVDecide.BoolExpr.literal var => Std.Tactic.BVDecide.BVPred.bitblast aig { val := var, cache := cache }
    | Std.Tactic.BVDecide.BoolExpr.const val =>
      { result := ⟨{ aig := aig, ref := aig.mkConstCached val }, ⋯⟩, cache := cache }
    | expr.not =>
      match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache with
      | { result := ⟨{ aig := aig_1, ref := exprRef }, hexpr⟩, cache := cache } =>
        let ret := aig_1.mkNotCached exprRef;
        have this := ⋯;
        have cache := cache.cast this;
        have this := ⋯;
        { result := ⟨ret, this⟩, cache := cache }
    | discr.ite lhs rhs =>
      match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig discr cache with
      | { result := ⟨{ aig := aig_1, ref := discrRef }, dextend⟩, cache := cache } =>
        match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig_1 lhs cache with
        | { result := ⟨{ aig := aig_2, ref := lhsRef }, lextend⟩, cache := cache } =>
          match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig_2 rhs cache with
          | { result := ⟨{ aig := aig_3, ref := rhsRef }, rextend⟩, cache := cache } =>
            let discrRef_1 := discrRef.cast ⋯;
            let lhsRef_1 := lhsRef.cast rextend;
            let input := { discr := discrRef_1, lhs := lhsRef_1, rhs := rhsRef };
            let ret := aig_3.mkIfCached input;
            have this := ⋯;
            have cache := cache.cast this;
            have this := ⋯;
            { result := ⟨ret, this⟩, cache := cache }
    | Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs =>
      match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig lhs cache with
      | { result := ⟨{ aig := aig_1, ref := lhsRef }, lextend⟩, cache := cache } =>
        match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig_1 rhs cache with
        | { result := ⟨{ aig := aig_2, ref := rhsRef }, rextend⟩, cache := cache } =>
          let lhsRef_1 := lhsRef.cast rextend;
          let input := { lhs := lhsRef_1, rhs := rhsRef };
          match g with
          | Std.Tactic.BVDecide.Gate.and =>
            let ret := aig_2.mkAndCached input;
            have this := ⋯;
            have cache := cache.cast this;
            have this := ⋯;
            { result := ⟨ret, this⟩, cache := cache }
          | Std.Tactic.BVDecide.Gate.xor =>
            let ret := aig_2.mkXorCached input;
            have this := ⋯;
            have cache := cache.cast this;
            have this := ⋯;
            { result := ⟨ret, this⟩, cache := cache }
          | Std.Tactic.BVDecide.Gate.beq =>
            let ret := aig_2.mkBEqCached input;
            have this := ⋯;
            have cache := cache.cast this;
            have this := ⋯;
            { result := ⟨ret, this⟩, cache := cache }
          | Std.Tactic.BVDecide.Gate.or =>
            let ret := aig_2.mkOrCached input;
            have this := ⋯;
            have cache := cache.cast this;
            have this := ⋯;
            { result := ⟨ret, this⟩, cache := cache }