aac_reflexivity leads to QED blow up in trivial case (just one unit removed) about aac-tactics HOT 7 CLOSED

test =
fun a : Z =>
@lift_reflexivity Z (@eq Z) (@eq Z)
  (@aac_lift_subrelation Z (@eq Z) (@eq Z) (@eq_equivalence Z) (@eq_Transitive Z)
     (@subrelation_refl Z (@eq Z))) (@eq_Reflexive Z) (Z.add a evil) (Z.add evil a)
  (let env_sym :=
     sigma_get
       {| Internal.Sym.ar := 0; Internal.Sym.value := evil; Internal.Sym.morph := proper_eq evil |}
       (sigma_add 1%positive
          {| Internal.Sym.ar := 0; Internal.Sym.value := a; Internal.Sym.morph := proper_eq a |}
          (sigma_empty Internal.Sym.pack)) in
   let env_bin :=
     sigma_get
       {|
         Internal.Bin.value := Z.add;
         Internal.Bin.compat := reflexive_proper Z.add;
         Internal.Bin.assoc := aac_Z_add_Assoc;
         Internal.Bin.comm := Some aac_Z_add_Comm;
         Internal.Bin.idem := None
       |} (sigma_empty Internal.Bin.pack) in
   let env_units :=
     sigma_get
       {|
         Internal.u_value := 0;
         Internal.u_desc := {| Internal.uf_idx := 1; Internal.uf_desc := aac_Z_add_0_Unit |} :: nil
       |} (sigma_empty (Internal.unit_pack env_bin)) in
   let tty := Internal.T env_sym in
   let rsum := Internal.sum (e_sym:=env_sym) in
   let rprd := Internal.prd (e_sym:=env_sym) in
   let rsym := Internal.sym (e_sym:=env_sym) in
   let vnil := Internal.vnil env_sym in
   let vcons := Internal.vcons (e_sym:=env_sym) in
   let eval := Internal.eval (e_sym:=env_sym) env_units in
   let left :=
     rsum 1%positive
       (Utils.cons (rsym 1%positive vnil, 1%positive) (Utils.nil (rsym 2%positive vnil, 1%positive)))
     in
   let right :=
     rsum 1%positive
       (Utils.cons (rsym 2%positive vnil, 1%positive) (Utils.nil (rsym 1%positive vnil, 1%positive)))
     in
   Internal.decide env_units left right
     (eq_refl : Internal.compare (Internal.norm env_units left) (Internal.norm env_units right) = Eq)
   <: (* VM CAST HERE, inferred type "Internal.eval env_units left = Internal.eval env_units right" *)
   a + evil = evil + a)
     : forall a : Z, a + evil = evil + a