val elim_lift_binrel (#a:Type) (r:binrel a) (y:top) (x:a)
  : Lemma
    (requires lift_binrel r y (| a, x |))
    (ensures dfst y == a /\ r (dsnd y) x)
let elim_lift_binrel (#a:Type) (r:binrel a) (y:top) (x:a)
  : Lemma
    (requires lift_binrel r y (| a, x |))
    (ensures dfst y == a /\ r (dsnd y) x)
  = let s : squash (lift_binrel r y (| a, x |)) = FStar.Squash.get_proof (lift_binrel r y (| a, x |)) in
    let s : squash (dfst y == a /\ r (dsnd y) x) = FStar.Squash.bind_squash s (fun (pf:lift_binrel r y (|a, x|)) ->
      let p1 : (dfst y == a /\ a == a) = dfst pf in
      let p2 : r (dsnd y) x = dsnd pf in
      introduce dfst y == a /\ r (dsnd y) x
      with eliminate dfst y == a /\ a == a
           returns _
           with l r. l
      and  FStar.Squash.return_squash p2)
    in
    ()
val elim_lift_binrel (#a:Type) (r:binrel a) (y:top) (x:a)
  : Lemma
    (requires lift_binrel r y (| a, x |))
    (ensures dfst y == a /\ r (dsnd y) x)
let elim_lift_binrel (#a: Type) (r: binrel a) (y: top) (x: a)
    : Lemma (requires lift_binrel r y (| a, x |)) (ensures dfst y == a /\ r (dsnd y) x) =
let s:squash (lift_binrel r y (| a, x |)) = FStar.Squash.get_proof (lift_binrel r y (| a, x |)) in
let s:squash (dfst y == a /\ r (dsnd y) x) =
  FStar.Squash.bind_squash s
    (fun (pf: lift_binrel r y (| a, x |)) ->
        let p1:(dfst y == a /\ a == a) = dfst pf in
        let p2:r (dsnd y) x = dsnd pf in
        introduce dfst y == a /\ r (dsnd y) x
        with eliminate dfst y == a /\ a == a
        returns _
        with l r . l
        and FStar.Squash.return_squash p2)
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 FStar.WellFounded.Util.top Prims.squash Prims.l_and Prims.eq2 FStar.Pervasives.dfst FStar.Pervasives.dsnd FStar.Squash.bind_squash FStar.WellFounded.Util.lift_binrel Prims.Mkdtuple2 FStar.Classical.Sugar.and_intro Prims.unit FStar.Classical.Sugar.and_elim FStar.Squash.return_squash FStar.Squash.get_proof 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)
    (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
    ()

let elim_lift_binrel (#a:Type) (r:binrel a) (y:top) (x:a)
  : Lemma
    (requires lift_binrel r y (| a, x |))
val elim_lift_binrel (#a:Type) (r:binrel a) (y:top) (x:a)
  : Lemma
    (requires lift_binrel r y (| a, x |))
    (ensures dfst y == a /\ r (dsnd y) x)
r: FStar.WellFounded.binrel a -> y: FStar.WellFounded.Util.top -> x: a
  -> FStar.Pervasives.Lemma (requires FStar.WellFounded.Util.lift_binrel r y (| a, x |))
      (ensures FStar.Pervasives.dfst y == a /\ r (FStar.Pervasives.dsnd y) x)