sub.v

From mathcomp Require Import ssreflect ssrbool ssrnat seq eqtype.

Inductive type :=
  | Int
  | Bool
  | Arrow of type & type.

Inductive sub : type -> type -> Set :=
  | sub_int : sub Int Int
  | sub_bool : sub Bool Bool
  | sub_bool_int : sub Bool Int
  | sub_arrow T1 T2 T1' T2' :
      sub T1' T1 ->
      sub T2 T2' ->
      sub (Arrow T1 T2) (Arrow T1' T2').

Hint Constructors sub.

Lemma sub_trans_aux T1 T2 :
  sub T1 T2 ->
  forall T3,
  (sub T2 T3 -> sub T1 T3) *
  (sub T3 T1 -> sub T3 T2).
Proof.
  induction 1 => ?; split; inversion 1; subst; constructor.
  - exact: (snd (IHsub1 _)).
  - exact: (fst (IHsub2 _)).
  - exact: (fst (IHsub1 _)).
  - exact: (snd (IHsub2 _)).
Defined.

Definition sub_trans T1 T2 (H : sub T1 T2) T3 :=
  fst (sub_trans_aux T1 T2 H T3).

Eval compute in (sub_trans _ _ sub_bool _ sub_bool_int).