fact: Fixpoint proj t := match t with | Var _ => t | Fun f ts => match pi f with | None => Fun f (Vmap proj ts) | Some o => let (_, h) := o in proj (Vnth ts h) end end.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)