unification issue with overly applied constant

[lecopivo]

Applying ftrans/fprop rules fails when a constant has more applied arguments then its normal number of arguments. For example Prof.fst has only one argument but Prod.fst (f,g) x has two applied arguments.

This issue is effectively a reverse situation of #9 when there are too few applied arguments

This should work

import SciLean

open SciLean

variable 
  {K : Type _} [IsROrC K]
  {α : Type _}

set_option trace.Meta.Tactic.simp.unify true
example (i : α) : IsDifferentiable K (fun (xy : (α → K) × (α → K)) => xy.fst i) := by fprop


set_option trace.Meta.Tactic.simp.unify true
example (i : α) 
  : cderiv K (fun (xy : (α → K) × (α → K)) => xy.fst i)
    =
    fun xy dxy => 
      dxy.1 i := by ftrans only