proposition: Lemma eq_can_Pi : forall (s : skel) (X Y : term -> Prop) (F1 F2 : Can (PROD s PROP)), eq_can PROP X Y -> eq_can (PROD s PROP) F1 F2 -> eq_can PROP (Pi s X F1) (Pi s Y F2).
proof: Proof. simpl in |- *; intros; unfold iff, Pi in |- *. split; intros. elim H0 with C C (App t u); elim H with u; auto with coc core arith datatypes. elim H0 with C C (App t u); elim H with u; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class