The filtering of parameters for builtin definitions happens after the computation of the implicit parameters

[sonmarcho]

trafficstars

First reported on the Zulip: https://aeneas-verif.zulipchat.com/#narrow/channel/349819-general/topic/Bugs.3A.20SHA1.20in.20Aeneas/near/493428308 This can lead to issues with external, non-builtin definitions, like here:

axiom alloc.vec.Vec.extend_from_slice
  {T : Type} {A : Type} (corecloneCloneInst : core.clone.Clone T) :
  --          ^^^^^^^^ This type parameter can't actually be infered from the inputs
  alloc.vec.Vec T → Slice T → Result (alloc.vec.Vec T)