Nuprl Lemma : agree_on_common_symmetry

[T:Type]. ∀as,bs:T List.  (agree_on_common(T;as;bs)  agree_on_common(T;bs;as))


Proof




Definitions occuring in Statement :  agree_on_common: agree_on_common(T;as;bs) list: List uall: [x:A]. B[x] all: x:A. B[x] implies:  Q universe: Type
Definitions unfolded in proof :  true: True so_apply: x[s1;s2;s3] top: Top so_lambda: so_lambda3 agree_on_common: agree_on_common(T;as;bs) so_apply: x[s] prop: implies:  Q so_lambda: λ2x.t[x] member: t ∈ T all: x:A. B[x] uall: [x:A]. B[x] or: P ∨ Q and: P ∧ Q cand: c∧ B not: ¬A false: False
Lemmas referenced :  cons_wf istype-universe list_ind_cons_lemma istype-void list_ind_nil_lemma nil_wf agree_on_common_wf list_wf all_wf list_induction l_member_wf
Rules used in proof :  universeEquality functionIsType rename natural_numberEquality voidElimination isect_memberEquality_alt dependent_functionElimination independent_functionElimination universeIsType inhabitedIsType because_Cache functionEquality hypothesis lambdaEquality_alt sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution unionElimination productElimination inrFormation_alt inlFormation_alt independent_pairFormation productIsType equalityIstype unionIsType equalitySymmetry

Latex:
\mforall{}[T:Type].  \mforall{}as,bs:T  List.    (agree\_on\_common(T;as;bs)  {}\mRightarrow{}  agree\_on\_common(T;bs;as))



Date html generated: 2020_05_20-AM-07_48_10
Last ObjectModification: 2020_01_24-PM-02_32_15

Theory : list!


Home Index