Handle types with parameters in automatic saturation

[gares]

TODO: detail steps by @CohenCyril

[gares]

• add pred has-mixin-instance o:cs-key, o:mixinname, o:gref. and store that instead of mixin-src in the data base
  • We already have a list of clauses like mixin-src Ty M I, we map it to a list of clauses has-mixin-instance K M Ihd where
    • term->gref Ty K and term->gref I Ihd
• from has-mixin-instance generate conditional clauses like mixin-src {{ list lp:T }} Mixin {{ src lp:I }} :- find-instance T Structure I where i : forall T : Structure, Mixin (list T)
  • use coq.unify with a well chosen problem to infer the structure on T, eg Structure.sort _ = T

[proux01]

Linked to #347