val exists_elim2
    (goal:Type) (#a:Type) (#b:(a -> Type)) (#p:(x:a -> b x -> Type))
    (_:squash (exists (x:a) (y:b x). p x y))
    (f:(x:a -> y:b x{p x y} -> GTot (squash goal)))
  : Lemma goal
let exists_elim2 goal #a #b #p _ f =
  let open FStar.Classical in
  exists_elim goal () (fun (x:a{exists (y:b x). p x y}) ->
    exists_elim goal () (fun (y:b x{p x y}) ->
      f x y))
val exists_elim2
    (goal:Type) (#a:Type) (#b:(a -> Type)) (#p:(x:a -> b x -> Type))
    (_:squash (exists (x:a) (y:b x). p x y))
    (f:(x:a -> y:b x{p x y} -> GTot (squash goal)))
  : Lemma goal
let exists_elim2 goal #a #b #p _ f =
let open FStar.Classical in
exists_elim goal
  ()
  (fun (x: a{exists (y: b x). p x y}) -> exists_elim goal () (fun (y: b x {p x y}) -> f x y))
Vale.Lib.Meta.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.Lib.Meta.fst
Prims.squash Prims.l_Exists FStar.Classical.exists_elim Prims.unit
module Vale.Lib.Meta
open FStar.Mul

let generic_injective_proof #a #b f g l =
  let helper (x x':a) : Lemma (f x == f x' ==> x == x') =
    if f x = f x' then
      if not (x = x') then (
        let y = f x in
        let y' = f x' in
        assert (y == y');
        let z = g y in
        let z' = g y' in
        assert (z == z');
        l x;
        assert (z == x);
        l x';
        assert (z' == x');
        ()
      ) else ()
    else
      ()
    in
  FStar.Classical.forall_intro_2 helper;
  ()
val exists_elim2
    (goal:Type) (#a:Type) (#b:(a -> Type)) (#p:(x:a -> b x -> Type))
    (_:squash (exists (x:a) (y:b x). p x y))
    (f:(x:a -> y:b x{p x y} -> GTot (squash goal)))
  : Lemma goal

    goal: Type0 ->
    _: Prims.squash (exists (x: a) (y: b x). p x y) ->
    f: (x: a -> y: b x {p x y} -> Prims.GTot (Prims.squash goal))
  -> FStar.Pervasives.Lemma (ensures goal)