[isabelle] One more lemma to add to Isabelle/ZF

I suggest one more lemma to add to Isabelle/ZF:
lemma comp_fun2: "[| g: A->B1; f: B0->C; B1<=B0 |] ==> (f O g) : A->C"
proof -
  assume "g: A->B1" "f: B0->C" "B1<=B0"
  with `g: A->B1` have "g: A->B0" by auto (rule fun_weaken_type)
  from `g: A->B0` `f: B0->C` show "(f O g) : A->C" by (rule comp_fun)

Victor Porton - http://portonvictor.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.