fact: Definition mk_arrow (o : option AF) (k: kind) (f1 f2: TFormula TX AF k) := match o with | None => IMPL f1 None f2 | Some _ => if is_X f1 then f2 else IMPL f1 o f2 end.
imports: List Refl Bool Relation_Definitions Setoid