proposition: Lemma ins_int_inv : forall (e f : intP) (k : nat) (y : Int_K), TIns _ y k e f -> int_inv f -> int_inv e.
proof: Proof. unfold int_inv, int_eq_can in |- *. simple induction 1; intros; auto with coc core arith datatypes. inversion_clear H0; auto with coc core arith datatypes. inversion_clear H2; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can