proposition: Lemma GAlphaInd: forall (P : forall gs : GSym G, Term gs -> Term gs -> [univ]) (PP : forall gs : GSym G, Pattern gs -> Pattern gs -> [univ]) (PA : Abstraction -> Abstraction -> [univ]) (PLA : list Abstraction -> list Abstraction -> [univ]), (forall (T : Terminal G) (t : tSemType G T), P (gsymT T) (tleaf T t) (tleaf T t)) -> (forall (V : VarSym G) (v : vType V), P (gsymTN (vSubstType G V)) (vleaf V v) (vleaf V v)) -> (forall (p : TermProd G) (ma mb : Mixture (tpRhsAugIsPat p)), lAlphaEqAbs (MakeAbstractions ma (allBndngVars vc p ma)) (MakeAbstractions mb (allBndngVars vc p mb)) -> PLA (MakeAbstractions ma (allBndngVars vc p ma)) (MakeAbstractions mb (allBndngVars vc p mb)) -> P (gsymTN (tpLhs G p)) (tnode p ma) (tnode p mb)) -> (forall (T : Terminal G) (t : tSemType G T), PP (gsymT T) (ptleaf T t) (ptleaf T t)) -> (forall (vcc : VarSym G) (vara varb : vType vcc), PP (gsymV vcc) (pvleaf vcc vara) (pvleaf vcc varb)) -> (forall (p : EmbedProd G) (nta ntb : Term (gsymTN (epRhs G p))), tAlphaEq nta ntb -> P (gsymTN (epRhs G p)) nta ntb -> PP (gsymPN (epLhs G p)) (embed p nta) (embed p ntb)) -> (forall (p : PatProd G) (ma mb : Mixture (map (fun x : GSym G => (true, x)) (ppRhsSym p))), lAlphaEqAbs (MakeAbstractions ma []) (MakeAbstractions mb []) -> PLA (MakeAbstractions ma []) (MakeAbstractions mb []) -> PP (gsymPN (ppLhs G p)) (pnode p ma) (pnode p mb)) -> (forall (gs : GSym G) (lbva lbvb lbnew : list vcType) (tma tmb : Term gs), let swapa := combine lbva lbnew in let swapb := combine lbvb lbnew in length lbva = length lbnew -> length lbvb = length lbnew -> tFresh lbnew [tma, tmb] -> disjoint (lbva ++ lbvb) lbnew -> tAlphaEq (tSwap tma swapa) (tSwap tmb swapb) -> P gs (tSwap tma swapa) (tSwap tmb swapb) -> PA (termAbs lbva tma) (termAbs lbvb tmb)) -> (forall (gs : GSym G) (lbva lbvb lbnew : list vcType) (tma tmb : Pattern gs), let swapa := combine lbva lbnew in let swapb := combine lbvb lbnew in length lbva = length lbnew -> length lbvb = length lbnew -> pFresh lbnew [tma, tmb] -> disjoint (lbva ++ lbvb) lbnew -> pAlphaEq (pSwap tma swapa) (pSwap tmb swapb) -> PP gs (pSwap tma swapa) (pSwap tmb swapb) -> PA (patAbs lbva tma) (patAbs lbvb tmb)) -> PLA [] [] -> (forall (ha hb : Abstraction) (la lb : list Abstraction), AlphaEqAbs ha hb -> PA ha hb -> lAlphaEqAbs la lb -> PLA la lb -> PLA (ha :: la) (hb :: lb)) -> ((forall (gs : GSym G) (ta tb : Term gs), tAlphaEq ta tb -> P gs ta tb) *(forall (gs : GSym G) (pa pb : Pattern gs), pAlphaEq pa pb -> PP gs pa pb) *(forall aa ab : Abstraction, AlphaEqAbs aa ab -> PA aa ab) *(forall la lb : list Abstraction, lAlphaEqAbs la lb -> PLA la lb) ).
proof: Proof. intros. dands. - eapply tAlphaEqMut; eauto. - eapply pAlphaEqMut; eauto. - eapply alphaEqAbsMut; eauto. - eapply lAlphaEqAbsMut; eauto. Defined.
imports: Swap