val generic_injective_proof
    (#a:eqtype) (#b:eqtype) (f:a -> b) (g:b -> a) (l:(x:a -> Lemma (g (f x) == x)))
  : Lemma (forall (x x':a).{:pattern f x; f x'} f x == f x' ==> x == x')
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 generic_injective_proof
    (#a:eqtype) (#b:eqtype) (f:a -> b) (g:b -> a) (l:(x:a -> Lemma (g (f x) == x)))
  : Lemma (forall (x x':a).{:pattern f x; f x'} f x == f x' ==> x == x')
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');
        ())
in
FStar.Classical.forall_intro_2 helper;
()
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.eqtype Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.Nil FStar.Pervasives.pattern FStar.Classical.forall_intro_2 Prims.l_imp Prims.op_Equality Prims.op_Negation Prims._assert Prims.bool
module Vale.Lib.Meta
open FStar.Mul
val generic_injective_proof
    (#a:eqtype) (#b:eqtype) (f:a -> b) (g:b -> a) (l:(x:a -> Lemma (g (f x) == x)))
  : Lemma (forall (x x':a).{:pattern f x; f x'} f x == f x' ==> x == x')
f: (_: a -> b) -> g: (_: b -> a) -> l: (x: a -> FStar.Pervasives.Lemma (ensures g (f x) == x))
  -> FStar.Pervasives.Lemma
    (ensures forall (x: a) (x': a). {:pattern f x; f x'} f x == f x' ==> x == x')