proposition: Lemma commut_red1_subterm : commut _ subterm (transp _ red1).
proof: Proof. red in |- *. simple induction 1; intros. inversion_clear H0. exists (Abs t z); auto with coc core arith sets. exists (Prod t z); auto with coc core arith sets. inversion_clear H0. exists (Abs z n); auto with coc core arith sets. exists (App z v); auto with coc core arith sets. exists (App u z); auto with coc core arith sets. exists (Prod z n); auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations