(reported by @nikswamy )
trefl fails on the following equality when removing indirection equalities in the first phase of the framing tactic
dlist_snoc left last cur right (List.Tot.Base.snoc ((*?u1592*) _ :: (*?u1588*) _, x)) ==
dlist_snoc left last cur right (List.Tot.Base.snoc (hd :: xs', x))
The failing file is https://github.com/FStarLang/FStar/blob/06af5727d3bad59b27df74418862b962b0416d31/examples/steel/DList.Invariant.fst#L249
The scope restriction removing hd/xs' from the context of ?u1592 and ?u1588 seems to come from the equality
(*?u439*) _ (id (Cons?.hd _)) (id (Cons?.tl _)) == (*?u418*) _
where ?u418 seems to be the inferred preresource of the match branch
(reported by @nikswamy )
trefl fails on the following equality when removing indirection equalities in the first phase of the framing tactic
The failing file is https://github.com/FStarLang/FStar/blob/06af5727d3bad59b27df74418862b962b0416d31/examples/steel/DList.Invariant.fst#L249
The scope restriction removing hd/xs' from the context of ?u1592 and ?u1588 seems to come from the equality
where ?u418 seems to be the inferred preresource of the match branch