proposition: Lemma adapt_int_inv : forall ip : intP, can_adapt ip -> int_inv ip.
proof: Proof. simple induction 1; simpl in |- *; auto with coc core arith datatypes. simple induction 1; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ