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: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ 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: P ⇒ 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: A 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