Selected Objects
| THM | decidable_iff_exists_bool_function |  P:(T  Prop). (x:T. Dec(P(x)))   ( f_p:(T ). x:T. P(x)  f_p(x)) |
| THM | decidable_iff_exists_bool_function_2 | P:(TZProp). (x:T, y:Z. Dec(P(x,y))) (f_p:(TZ). x:T, y:Z. P(x,y) f_p(x,y)) |
| THM | sq_stable_functionality_wrt_or | SqStable(P) SqStable(Q) SqStable(P  Q) SqStable(P) SqStable(Q) |
| THM | sq_stable__or | Dec(P) Dec(Q) SqStable(P Q) |
| THM | decidable_functionality_wrt_iff | (P Q) (Dec(P) Dec(Q)) |
| THM | decidable__true | Dec(True) |
| THM | decidable__equal_nil | Dec(nil = nil  T List) |
| THM | demorgan | Dec(P) Dec(Q) ( (P Q) P & Q) |
| THM | demorgan1 | Dec(P) Dec(Q) ((P Q) P & Q) |
| THM | demorgan2 | Dec(P) Dec(Q) ((P & Q) P Q) |
| THM | contrapositive | Dec(P) Dec(Q) ((P Q) (Q P)) |
| THM | pair_functionality_wrt_equal | t1,t2:T, u1,u2:U. t1 = t2 u1 = u2 < t1,u1 > = < t2,u2 > |
| def | equivalence | {T  } == {f:(TT)| (x:T. f(x,x)) & (x,y:T. f(x,y) f(y,x)) & (x,y,z:T. f(x,y) f(y,z) f(x,z)) } |
| THM | equivalence_inc | {T}  (TT) |
| THM | discrete_equality_inc_equivalence | {T=} {T} |
| THM | equivalence_type | eq:{T}. eq TT |
| THM | equivalence_properties | f:{T}. (x,y,z:T. f(x,y) f(y,z) f(x,z)) & (x,y:T. f(x,y) f(y,x)) & (x:T. f(x,x)) & f TT |
| THM | equivalence_symmetric | eq:{T}, x,y:T. eq(x,y) eq(y,x) |
| THM | equivalence_bool_function | eq:{T}. eq TT |
| THM | equivalence_reflexive | eq:{T}, u:T. eq(u,u) |
| THM | discrete_equality_is_equivalence | EQ:{T=}. EQ {T} |
| THM | equivalence_weakening_lemma | eq:{T=}, f:{T}, x,y:T. eq(x,y) f(x,y) |
| THM | not_equivalence_implies_not_discrete_eq | eq:{T}, f:{T=}, x,y:T. eq(x,y) f(x,y) |
| THM | decidable__spread | P:(TUProp). (x:T, y:U. Dec(P(x,y))) (p:(T U). Dec(p/l,r. P(l,r))) |
| THM | not_not_rw | P:(TProp). (x:T. Dec(P(x))) (x:T. P(x) P(x)) |