---

Step * of Lemma RankEx1_ind_wf_simple

∀[T,A:Type]. ∀[v:RankEx1(T)]. ∀[Leaf:leaf:T ⟶ A]. ∀[Prod:prod:(RankEx1(T) × RankEx1(T))
                                                          ⟶ let u,u1 = prod 
                                                             in A ∧ A
                                                          ⟶ A]. ∀[ProdL:prodl:(T × RankEx1(T))
                                                                         ⟶ let u,u1 = prodl 
                                                                            in A
                                                                         ⟶ A]. ∀[ProdR:prodr:(RankEx1(T) × T)
                                                                                        ⟶ let u,u1 = prodr 
                                                                                           in A
                                                                                        ⟶ A].
∀[List:list:(RankEx1(T) List) ⟶ (∀u∈list.A) ⟶ A].
  (RankEx1_ind(v;
               RankEx1_Leaf(leaf)⇒ Leaf[leaf];
               RankEx1_Prod(prod)⇒ rec1.Prod[prod;rec1];
               RankEx1_ProdL(prodl)⇒ rec2.ProdL[prodl;rec2];
               RankEx1_ProdR(prodr)⇒ rec3.ProdR[prodr;rec3];
               RankEx1_List(list)⇒ rec4.List[list;rec4])  ∈ A)
BY
{ ProveDatatypeIndWfSimple 1 `RankEx1_ind_wf` }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[v:RankEx1(T)].  \mforall{}[Leaf:leaf:T  {}\mrightarrow{}  A].  \mforall{}[Prod:prod:(RankEx1(T)  \mtimes{}  RankEx1(T))
                                                                                                                    {}\mrightarrow{}  let  u,u1  =  prod 
                                                                                                                          in  A  \mwedge{}  A
                                                                                                                    {}\mrightarrow{}  A].  \mforall{}[ProdL:prodl:(T  \mtimes{}  RankEx1(T))
                                                                                                                                                  {}\mrightarrow{}  let  u,u1  =  prodl 
                                                                                                                                                        in  A
                                                                                                                                                  {}\mrightarrow{}  A].
\mforall{}[ProdR:prodr:(RankEx1(T)  \mtimes{}  T)  {}\mrightarrow{}  let  u,u1  =  prodr  in  A  {}\mrightarrow{}  A].  \mforall{}[List:list:(RankEx1(T)  List)
                                                                                                                                            {}\mrightarrow{}  (\mforall{}u\mmember{}list.A)
                                                                                                                                            {}\mrightarrow{}  A].
    (RankEx1\_ind(v;
                              RankEx1\_Leaf(leaf){}\mRightarrow{}  Leaf[leaf];
                              RankEx1\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;rec1];
                              RankEx1\_ProdL(prodl){}\mRightarrow{}  rec2.ProdL[prodl;rec2];
                              RankEx1\_ProdR(prodr){}\mRightarrow{}  rec3.ProdR[prodr;rec3];
                              RankEx1\_List(list){}\mRightarrow{}  rec4.List[list;rec4])    \mmember{}  A)


By

---

Latex:
ProveDatatypeIndWfSimple  1  `RankEx1\_ind\_wf`

---

Home Index