val lemma_pointwise_equal (a b:poly) (pf:(i:int -> Lemma (a.[i] == b.[i]))) : Lemma
  (a == b)
let lemma_pointwise_equal a b pf =
  FStar.Classical.forall_intro pf;
  lemma_equal a b
val lemma_pointwise_equal (a b:poly) (pf:(i:int -> Lemma (a.[i] == b.[i]))) : Lemma
  (a == b)
let lemma_pointwise_equal a b pf =
FStar.Classical.forall_intro pf;
lemma_equal a b
Vale.Math.Poly2.Lemmas.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.List.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Math.Poly2.Lemmas.fst
Vale.Math.Poly2_s.poly Prims.int Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.bool Vale.Math.Poly2_s.op_String_Access Prims.Nil FStar.Pervasives.pattern Vale.Math.Poly2.lemma_equal FStar.Classical.forall_intro
module Vale.Math.Poly2.Lemmas
open FStar.Mul
val lemma_pointwise_equal (a b:poly) (pf:(i:int -> Lemma (a.[i] == b.[i]))) : Lemma
  (a == b)

    a: Vale.Math.Poly2_s.poly ->
    b: Vale.Math.Poly2_s.poly ->
    pf: (i: Prims.int -> FStar.Pervasives.Lemma (ensures a.[ i ] == b.[ i ]))
  -> FStar.Pervasives.Lemma (ensures a == b)