val intro_lift_binrel (#a:Type) (r:binrel a) (y:a) (x:a)
  : Lemma
    (requires r y x)
    (ensures lift_binrel r (| a, y |) (| a, x |))
let intro_lift_binrel (#a:Type) (r:binrel a) (y:a) (x:a)
  : Lemma
    (requires r y x)
    (ensures lift_binrel r (| a, y |) (| a, x |))
  = let t0 : top = (| a, y |) in
    let t1 : top = (| a, x |) in
    let pf1 : squash (dfst t0 == a /\ dfst t1 == a) = () in
    let pf2 : squash (r (dsnd t0) (dsnd t1)) = () in
    let pf : squash (lift_binrel r t0 t1) =
      FStar.Squash.bind_squash pf1 (fun (pf1: (dfst t0 == a /\ dfst t1 == a)) ->
      FStar.Squash.bind_squash pf2 (fun (pf2: (r (dsnd t0) (dsnd t1)))  ->
      let p : lift_binrel r t0 t1 = (| pf1, pf2 |) in
      FStar.Squash.return_squash p))
    in
    ()
val intro_lift_binrel (#a:Type) (r:binrel a) (y:a) (x:a)
  : Lemma
    (requires r y x)
    (ensures lift_binrel r (| a, y |) (| a, x |))
let intro_lift_binrel (#a: Type) (r: binrel a) (y x: a)
    : Lemma (requires r y x) (ensures lift_binrel r (| a, y |) (| a, x |)) =
let t0:top = (| a, y |) in
let t1:top = (| a, x |) in
let pf1:squash (dfst t0 == a /\ dfst t1 == a) = () in
let pf2:squash (r (dsnd t0) (dsnd t1)) = () in
let pf:squash (lift_binrel r t0 t1) =
  FStar.Squash.bind_squash pf1
    (fun (pf1: (dfst t0 == a /\ dfst t1 == a)) ->
        FStar.Squash.bind_squash pf2
          (fun (pf2: (r (dsnd t0) (dsnd t1))) ->
              let p:lift_binrel r t0 t1 = (| pf1, pf2 |) in
              FStar.Squash.return_squash p))
in
()
FStar.WellFounded.Util.fst.checked
prims.fst.checked FStar.WellFounded.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.StrongExcludedMiddle.fst.checked FStar.Squash.fsti.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked
FStar.WellFounded.Util.fst
FStar.WellFounded.binrel Prims.squash FStar.WellFounded.Util.lift_binrel FStar.Squash.bind_squash Prims.l_and Prims.eq2 FStar.Pervasives.dfst FStar.Pervasives.dsnd FStar.Squash.return_squash Prims.Mkdtuple2 FStar.WellFounded.Util.top Prims.unit Prims.Nil FStar.Pervasives.pattern
module FStar.WellFounded.Util
open FStar.WellFounded

#push-options "--warn_error -242" //inner let recs not encoded to SMT; ok

let intro_lift_binrel (#a:Type) (r:binrel a) (y:a) (x:a)
  : Lemma
    (requires r y x)
val intro_lift_binrel (#a:Type) (r:binrel a) (y:a) (x:a)
  : Lemma
    (requires r y x)
    (ensures lift_binrel r (| a, y |) (| a, x |))
r: FStar.WellFounded.binrel a -> y: a -> x: a
  -> FStar.Pervasives.Lemma (requires r y x)
      (ensures FStar.WellFounded.Util.lift_binrel r (| a, y |) (| a, x |))