### Nuprl Lemma : rel_path_wf

`∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[x,y:A]. ∀[L:(a:A × b:A × (R a b)) List].  (rel_path(A;L;x;y) ∈ ℙ)`

Proof

Definitions occuring in Statement :  rel_path: `rel_path(A;L;x;y)` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` rel_path: `rel_path(A;L;x;y)` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `so_lambda(x,y,z.t[x; y; z])` and: `P ∧ Q` pi1: `fst(t)` pi2: `snd(t)` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  list_ind_wf equal_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule applyEquality thin instantiate extract_by_obid sqequalHypSubstitution isectElimination productEquality cumulativity hypothesisEquality because_Cache functionExtensionality hypothesis lambdaEquality functionEquality universeEquality productElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[x,y:A].  \mforall{}[L:(a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List].    (rel\_path(A;L;x;y)  \mmember{}  \mBbbP{})

Date html generated: 2017_04_17-AM-09_25_35
Last ObjectModification: 2017_02_27-PM-05_26_14

Theory : relations2

Home Index