val lower_binrel (#a:Type)
                 (#r:binrel a)
                 (x y:top)
                 (p:lift_binrel r x y)
  : r (dsnd x) (dsnd y)
let lower_binrel (#a:Type)
                 (#r:binrel a)
                 (x y:top)
                 (p:lift_binrel r x y)
  : r (dsnd x) (dsnd y)
  = dsnd p
val lower_binrel (#a:Type)
                 (#r:binrel a)
                 (x y:top)
                 (p:lift_binrel r x y)
  : r (dsnd x) (dsnd y)
let lower_binrel (#a: Type) (#r: binrel a) (x y: top) (p: lift_binrel r x y) : r (dsnd x) (dsnd y) =
dsnd p
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 FStar.WellFounded.Util.lift_binrel FStar.Pervasives.dsnd Prims.l_and Prims.eq2 FStar.Pervasives.dfst
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 |))
    (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
    ()

let lower_binrel (#a:Type)
                 (#r:binrel a)
                 (x y:top)
                 (p:lift_binrel r x y)
val lower_binrel (#a:Type)
                 (#r:binrel a)
                 (x y:top)
                 (p:lift_binrel r x y)
  : r (dsnd x) (dsnd y)

    x: FStar.WellFounded.Util.top ->
    y: FStar.WellFounded.Util.top ->
    p: FStar.WellFounded.Util.lift_binrel r x y
  -> r (FStar.Pervasives.dsnd x) (FStar.Pervasives.dsnd y)