proposition: Lemma tr_apps : forall n (us : Tes n) E t T (hn : n <= arity T), tr E t T -> (forall i (hi : i < n), tr E (Vnth us hi) (Vnth (inputs T) (Nat.lt_le_trans hi hn))) -> tr E (apps t us) (output T n).
proof: Proof. induction us; intros E t T hn ht g. hyp. rename h into u. simpl. destruct T as [b|A B]; simpl in hn. lia. apply IHus with (hn := le_S_n hn). apply tr_app with A. hyp. gen (g _ (Nat.lt_0_succ n)). simpl. auto. intros i hi. gen (g _ (NatCompat.lt_n_S hi)). simpl. rewrite lt_unique with (h1 := NatCompat.lt_S_n (NatCompat.lt_n_S hi)) (h2 := hi). rewrite lt_unique with (h1 := NatCompat.lt_S_n _) (h2 := Nat.lt_le_trans hi (le_S_n hn)). auto. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)