Nuprl Lemma : fpf-union-compatible_symmetry

[A:Type]. ∀[B:A ─→ Type]. ∀[C:Type].
  ∀eq:EqDecider(A). ∀f,g:x:A fp-> B[x] List. ∀R:(C List) ─→ C ─→ 𝔹.
    (fpf-union-compatible(A;C;x.B[x];eq;R;f;g)  fpf-union-compatible(A;C;x.B[x];eq;R;g;f)) 
  supposing ∀a:A. (B[a] ⊆C)


Proof




Definitions occuring in Statement :  fpf-union-compatible: fpf-union-compatible(A;C;x.B[x];eq;R;f;g) fpf: a:A fp-> B[a] deq: EqDecider(T) list: List bool: 𝔹 uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ─→ B[x] universe: Type
Lemmas :  l_member_wf fpf-ap_wf list_wf subtype_rel_list not_wf assert_wf or_wf fpf-dom_wf subtype-fpf2 top_wf subtype_top fpf-union-compatible_wf bool_wf fpf_wf deq_wf all_wf subtype_rel_wf
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[C:Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f,g:x:A  fp->  B[x]  List.  \mforall{}R:(C  List)  {}\mrightarrow{}  C  {}\mrightarrow{}  \mBbbB{}.
        (fpf-union-compatible(A;C;x.B[x];eq;R;f;g)  {}\mRightarrow{}  fpf-union-compatible(A;C;x.B[x];eq;R;g;f)) 
    supposing  \mforall{}a:A.  (B[a]  \msubseteq{}r  C)



Date html generated: 2015_07_17-AM-09_16_49
Last ObjectModification: 2015_01_28-AM-07_52_06

Home Index