val destruct_lhs_pairs (t: FStar.Tactics.term) (n: nat) : FStar.Tactics.Tac unit
let rec destruct_lhs_pairs (t: FStar.Tactics.term) (n: nat) : FStar.Tactics.Tac unit =
  if n = 0
  then trefl ()
  else begin
    destruct t;
    let a = intro () in
    let b = intro () in
    let abeq = intro () in
    rewrite abeq;
    destruct_lhs_pairs (binder_to_term a) (n - 1)
  end
val destruct_lhs_pairs (t: FStar.Tactics.term) (n: nat) : FStar.Tactics.Tac unit
let rec destruct_lhs_pairs (t: FStar.Tactics.term) (n: nat) : FStar.Tactics.Tac unit =
if n = 0
then trefl ()
else
  (destruct t;
    let a = intro () in
    let b = intro () in
    let abeq = intro () in
    rewrite abeq;
    destruct_lhs_pairs (binder_to_term a) (n - 1))
LowParse.Spec.Tac.Combinators.fst.checked
prims.fst.checked LowParse.TacLib.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked
LowParse.Spec.Tac.Combinators.fst
FStar.Reflection.Types.term Prims.nat Prims.op_Equality Prims.int FStar.Tactics.V1.Derived.trefl Prims.unit Prims.bool LowParse.Spec.Tac.Combinators.destruct_lhs_pairs Prims.op_Subtraction FStar.Tactics.V1.Derived.binder_to_term FStar.Tactics.V1.Builtins.rewrite FStar.Reflection.Types.binder FStar.Tactics.V1.Builtins.intro FStar.Tactics.V1.Derived.destruct
module LowParse.Spec.Tac.Combinators
include LowParse.Spec.Combinators

open LowParse.TacLib

(* for structs *)
val destruct_lhs_pairs (t: FStar.Tactics.term) (n: nat) : FStar.Tactics.Tac unit
t: FStar.Reflection.Types.term -> n: Prims.nat -> FStar.Tactics.Effect.Tac Prims.unit