proposition: Lemma GInductionS : forall {G: CFGV} (PT : forall g : GSym G, Term g -> [univ]) (PP : forall g : GSym G, Pattern g -> [univ]) (PM : forall l : MixtureParam, Mixture l -> [univ]), (forall (T : Terminal G) (t : tSemType G T), PT (gsymT T) (tleaf T t)) -> (forall (vc : VarSym G) (v : vType vc), PT (gsymTN (vSubstType G vc)) (vleaf vc v)) -> (forall (p : TermProd G) (m : Mixture (tpRhsAugIsPat p)), PM (tpRhsAugIsPat p) m -> PT (gsymTN (tpLhs G p)) (tnode p m)) -> (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 : EmbedProd G) (t : Term (gsymTN (epRhs G p))), PT (gsymTN (epRhs G p)) t -> PP (gsymPN (epLhs G p)) (embed p t)) -> (forall (p : PatProd G) (m : Mixture (map (fun x : GSym G => (true, x)) (ppRhsSym p))), PM (map (fun x : GSym G => (true, x)) (ppRhsSym p)) m -> PP (gsymPN (ppLhs G p)) (pnode p m)) -> PM [] mnil -> (forall (h : GSym G) (tl : MixtureParam) (ph : Term h), (forall (phnew:Term h), tSize phnew <= tSize ph -> PT h phnew) -> forall ptl : Mixture tl, PM tl ptl -> PM ((false, h) :: tl) (mtcons ph ptl)) -> (forall (h : GSym G) (tl : MixtureParam) (ph : Pattern h), (forall (phnew:Pattern h), pSize phnew <= pSize ph -> PP h phnew) -> forall ptl : Mixture tl, PM tl ptl -> PM ((true, h) :: tl) (mpcons ph ptl)) -> ((forall (g : GSym G) (p : Term g), PT g p) * (forall (g : GSym G) (p : Pattern g), PP g p) * (forall (l : list (bool # GSym G)) (m : Mixture l), PM l m)).
proof: Proof. introns Hyps. assert( forall n: nat, ( (forall (g : GSym G) (p : Term g), (tSize p = n) -> PT g p) * (forall (g : GSym G) (p : Pattern g), (pSize p = n) -> PP g p) * (forall (l : list (bool # GSym G)) (m : Mixture l), (mSize m = n) -> PM l m) )) as XX; [| dands; intros; try(apply ((tcase (XX _)) _ _ eq_refl)); try(apply ((pcase (XX _)) _ _ eq_refl)); try(apply ((mcase (XX _)) _ _ eq_refl)); fail]. induction n as [n Hind] using comp_ind_type. GInduction; introns HGInd; allsimpl; cpx. - Case "pembed". apply Hyps4. specialize (Hind (tSize t)). dimp Hind; try omega;[]. repnd. cpx. - Case "mtcons". apply Hyps7. + introv Hlt. pose proof (mcase SizePositive _ ptl). specialize (Hind (tSize phnew)). dimp Hind; try omega;[]. repnd. cpx. + pose proof (tcase SizePositive _ ph). specialize (Hind (mSize ptl)). dimp Hind; try omega;[]. repnd. cpx. - Case "mpcons". apply Hyps8. + introv Hlt. pose proof (mcase SizePositive _ ptl). specialize (Hind (pSize phnew)). dimp Hind; try omega;[]. repnd. cpx. + pose proof (pcase SizePositive _ ph). specialize (Hind (mSize ptl)). dimp Hind; try omega;[]. repnd. cpx. Defined.
imports: CFGV Omega