proposition: Lemma PatIndNoEmbed : forall (PP : forall g : GSym G, Pattern g -> [univ]), (EmbedProd G-> False) -> (forall (T : Terminal G) (t : tSemType G T), PP (gsymT T) (ptleaf T t)) -> (forall (vc : VarSym G) (v : vType vc), PP (gsymV vc) (pvleaf vc v)) -> (forall (p : PatProd G) (m : Mixture (map (fun x : GSym G => (true, x)) (ppRhsSym p))), (forall (s : GSym G) (pt : Pattern s), PatInMix pt m -> PP s pt) -> PP (gsymPN (ppLhs G p)) (pnode p m)) -> (forall (g : GSym G) (p : Pattern g), PP g p).
proof: Proof. introv Hnod Ht Hv Hem. induction p using pat_mut with (P:=(fun x y=> True)) (P1:= (fun l m=> (forall (s : GSym G) (pt : Pattern s), PatInMix pt m -> PP s pt))); auto; try contradiction. - introv Hin. simpl in Hin. dorn Hin. + exrepnd. unfold transport in Hin0. generalize dependent pt. rw p0. simpl. intros. auto. rw Hin0. auto. + apply IHp0. auto. Qed.
imports: CFGV Omega