fact: Fixpoint liftRelPtwise {T : Type} {G : CFGV} {lgs : MixtureParam} (ft: forall (gs : (GSym G)) (p : Term gs), T -> [univ]) (fp: forall (gs : (GSym G)) (p : Pattern gs), T -> [univ]) (pts : Mixture lgs) (l : list T) : [univ]:= match (pts,l) with | (mnil,[]) => True | (mtcons sh _ th ttl, lh::ltl) => (ft sh th lh)#(liftRelPtwise ft fp ttl ltl) | (mpcons sh _ th ttl, lh::ltl) => (fp sh th lh)#(liftRelPtwise ft fp ttl ltl) | _ => False end.
imports: CFGV Omega