proposition: Lemma TermIndNoPat : forall (PT : forall g : GSym G, Term g -> [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)), (forall (s : GSym G) (pt : Term s), TermInMix pt m -> PT s pt) -> PT (gsymTN (tpLhs G p)) (tnode p m)) -> (forall (g : GSym G) (p : Term g), PT g p).
proof: Proof. introv Ht Hv Hem. induction p using term_mut with (P0:=(fun x y=> True)) (P1:= (fun l m=> (forall (s : GSym G) (tt : Term s), TermInMix tt m -> PT s tt))); auto; try contradiction. - introv Hin. simpl in Hin. dorn Hin. + exrepnd. unfold transport in Hin0. generalize dependent tt. rw p0. simpl. intros. auto. rw Hin0. auto. + apply IHp0. auto. Qed.
imports: CFGV Omega