Found a weird bug in F*, line 35

Sandbox.fst

module Sandbox
module CE = FStar.Algebra.CommMonoid.Equiv
module SProp = FStar.Seq.Properties
module SB = FStar.Seq.Base
module SP = FStar.Seq.Permutation

type under (x:nat) = (t:nat{t<x})

let is_left_distributive #c #eq (mul add: CE.cm c eq) = 
  forall (x y z: c). mul.mult x (add.mult y z) `eq.eq` add.mult (mul.mult x y) (mul.mult x z)

let is_right_distributive #c #eq (mul add: CE.cm c eq) = 
  forall (x y z: c). mul.mult (add.mult x y) z `eq.eq` add.mult (mul.mult x z) (mul.mult y z)

let is_fully_distributive #c #eq (mul add: CE.cm c eq) = is_left_distributive mul add /\ is_right_distributive mul add

let is_absorber #c #eq (z:c) (op: CE.cm c eq) = 
  forall (x:c). op.mult z x `eq.eq` z /\ op.mult x z `eq.eq` z
 
let const_op_seq #c #eq (cm: CE.cm c eq) (const: c) (s: SB.seq c) 
  = SB.init (SB.length s) (fun (i: under (SB.length s)) -> cm.mult const (SB.index s i))
 
#restart-solver
let rec minimal_example #c #eq (mul add: CE.cm c eq) (a: c) (s: SB.seq c)
  : Lemma (requires is_fully_distributive mul add /\ is_absorber add.unit mul) 
          (ensures mul.mult a (SP.foldm_snoc add s) `eq.eq`
                   SP.foldm_snoc add (const_op_seq mul a s))
          (decreases SB.length s) = 
  if SB.length s > 0 then 
  let ((+), ( * ), (=)) = add.mult, mul.mult, eq.eq in
  let liat, last = SProp.un_snoc s in 
  minimal_example mul add a liat; 
  // Replace `eq.eq` with = below, and everything is good.
  // What is happening? 0_0
  assert (a * (SP.foldm_snoc add liat) `eq.eq` SP.foldm_snoc add (const_op_seq mul a liat));
  admit();
  ()