val poly_equal (a b: poly) : prop0
let poly_equal (a b:poly) : prop0 =
  (forall (i:nat).{:pattern a.[i] \/ b.[i]} a.[i] == b.[i])
val poly_equal (a b: poly) : prop0
let poly_equal (a b: poly) : prop0 =
(forall (i: nat). {:pattern a.[ i ]\/b.[ i ]} a.[ i ] == b.[ i ])
Vale.Math.Poly2.Defs.fst.checked
Vale.Math.Poly2.Defs_s.fst.checked Vale.Def.Prop_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Classical.fsti.checked
Vale.Math.Poly2.Defs.fst
Vale.Math.Poly2.Defs_s.poly Prims.l_Forall Prims.nat Prims.eq2 Prims.bool Vale.Math.Poly2.Defs_s.op_String_Access Vale.Def.Prop_s.prop0
module Vale.Math.Poly2.Defs
open FStar.Mul
open Vale.Def.Prop_s
open FStar.Seq
open Vale.Math.Poly2.Defs_s
unfold let max = FStar.Math.Lib.max

#reset-options "--z3rlimit 10"
val poly_equal (a b: poly) : prop0
a: Vale.Math.Poly2.Defs_s.poly -> b: Vale.Math.Poly2.Defs_s.poly -> Vale.Def.Prop_s.prop0