### Nuprl Lemma : comb_for_sublist_wf

`λT,L1,L2,z. L1 ⊆ L2 ∈ T:Type ⟶ L1:(T List) ⟶ L2:(T List) ⟶ (↓True) ⟶ ℙ`

Proof

Definitions occuring in Statement :  sublist: `L1 ⊆ L2` list: `T List` prop: `ℙ` squash: `↓T` true: `True` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ`
Lemmas referenced :  sublist_wf squash_wf true_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaEquality_alt,  sqequalHypSubstitution imageElimination cut introduction extract_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry Error :universeIsType,  Error :inhabitedIsType,  universeEquality

Latex:
\mlambda{}T,L1,L2,z.  L1  \msubseteq{}  L2  \mmember{}  T:Type  {}\mrightarrow{}  L1:(T  List)  {}\mrightarrow{}  L2:(T  List)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}

Date html generated: 2019_06_20-PM-01_22_38
Last ObjectModification: 2018_09_29-PM-00_28_16

Theory : list_1

Home Index